# The `h1` Tool Suite ### Jean Goubault-Larrecq
LSV/UMR 8643, CNRS, ENS Cachan & INRIA Futurs projet SECSI
61 avenue du président-Wilson, F-94235 Cachan Cedex
`goubault@lsv.ens-cachan.fr`
Phone: +33-1 47 40 75 68 Fax: +33-1 47 40 75 21

> 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 H1 class due to Nielson, Nielson, and Seidl. Alternatively, this can also be seen as a terminating automated theorem prover for the H1 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 H1 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 LATEX by HEVEA.