The h1 Tool Suite

Abstract: This describes the theoretical basis and practical usage of the h1 tool suite. This is a set of tools that allow one to handle tree-regular languages in various formats, including deterministic, non-deterministic, and alternating finite tree automata, but also various fairly general clausal formats, the central one being the H₁ class due to Nielson, Nielson, and Seidl. Alternatively, this can also be seen as a terminating automated theorem prover for the H₁ class; or as an automated theorem prover for general clause sets, which however makes some controlled mistakes in the spirit of abstract interpretation: this is notably useful in proofs of security protocols. Other aspects of the h1 tool suite include producing certain forms of automated proofs by induction in the Coq proof assistant, deciding Presburger arithmetic, and displaying tree automata.

• 1  Introduction
• 2  Tree Automata, Clauses
• 3  The h1 Tool Suite through Examples
  • 3.1  A Toy, Introductory Example
  • 3.2  The Dreadsbury Mansion Murder Mystery Example
  • 3.3  Computing with Tree Automata
    • 3.3.1  Visualizing Tree Automata
    • 3.3.2  Computing Intersections of Tree Automata
    • 3.3.3  Checking Tree Automata for Emptiness, Testing Membership
    • 3.3.4  Converting Alternating to Non-Deterministic Tree Automata
    • 3.3.5  Purging Tree Automata
    • 3.3.6  Determinizing Tree Automata
    • 3.3.7  Computing Unions, Transitive Closures
    • 3.3.8  Complete Deterministic Tree Automata, Taking Complements
  • 3.4  The Needham-Schroeder Symmetric Key Protocol Example
• 4  The h1 Prover
  • 4.1  How to Use h1
  • 4.2  Theoretical Background
  • 4.3  Principle of Operation
• 5  Explaining and Checking Proofs: h1trace, h1logstrip
• 6  Model-Checking Clause Sets and Explaining the Absence of Proofs with h1mc
  • 6.1  Theoretical Background
• 7  Determinizing Tree Automata with pldet
• 8  Converting XML Deterministic Tree Automata to Prolog Notation with auto2pl
• 9  Cleaning and Extracting Automata with plpurge
• 10  Converting Tree Automata and Prolog Programs to TPTP Files
• 11  Applying Morphisms to H₁ Clause Sets with tptpmorph
• 12  Solving Presburger Arithmetic Formulas with linauto
• 13  Displaying Automata with pl2gastex
• 14  Log Files and h1getlog
• 15  Bugs
  • There is no DTD for deterministic tree automata in XML format.
  • h1 works for a long time, then gets “Killed”
  • Clause names are lost in converting clauses to Prolog format.
• References
• Concept Index
• Command Index

This document was translated from L^AT_EX by H^EV^EA.