## 1 Introduction

The `h1` tool suite is a toolchest for handling finite tree automata, in various forms. There are basically three forms, from most constrained to least constrained:

1. as deterministic bottom-up tree automata;
2. as alternating tree automata;
3. as pure Prolog programs (sets of Horn clauses) in the H1 class [2002 (Nielson et al.)].

The global architecture is given in the following figure. Some things are still missing from it, and we will add them progressively later. The inner dashed box forms the core of the `h1` tool suite. The outer dashed box is the `h1` tool suite itself.
The main thing to understand is that the `h1` tool suite includes tools to convert between all three formats of tree automata, forming the core of the `h1` tool suite. The tools `h1`, `pldet`, `auto2pl`, `pl2tptp` are used to navigate between all three formats.
In the `h1` tool suite, deterministic tree automata are represented in files in XML format.
Alternating tree automata are represented as Horn clauses, in Prolog notation; in particular, you can run them in any Prolog implementation (whatever the use of this may be).
Finally, H1 clause sets are represented in TPTP format. TPTP (a Thousand Problems for Theorem Provers) is a publicly available repository used to test automated theorem provers, due to [2002 (Suttner and Sutcliffe)]. The `h1` tool suite handles TPTP input files that contain only clauses. This allows you to use any automated, clausal theorem prover in place of the `h1` prover if you so wish. The `h1` prover, one of the tools of the `h1` tool suite, is an automated theorem prover. In addition to searching for proofs, it is also able to produce counter-models and describe them as alternating tree automata; `h1` is described in Section 4.
Additional tools operate on such counter-models and proofs. They form the rest of the `h1` tool suite. As far as proofs are concerned, the `h1` tool keeps a trace of all proof steps it did in a trace log. This trace log is in a proprietary format that the `h1trace` and `h1logstring` tools can work on. (Don't assume anything on this format, it may change in the future.) This is pictured in the following figure.
The purpose of `h1trace` is to explain the proofs found by `h1`, both to humans, as a proof in natural deduction in text format, and to machines, as a formal proof, in Coq notation. Coq is a proof assistant developed in the LogiCal team at INRIA Futurs [1999–2003 (Barras et al.)].
The `h1` tool is also able to work on general clause sets, not just in the H1 format. In this case, `h1` will output a proof candidate, which however may fail to be a proof. In case this is a wrong proof, `h1trace` will do its best to explain the wrong proof to humans. This can be used to design a true proof.
In case a prover does not find a proof of some given query, you usually have no choice but to trust it that there is indeed no proof. In case `h1` does not find a proof of some given query, it outputs a model. This model can be independently checked by the `h1mc` model-checking tool; `h1mc` takes as input both a description of the model M, as an alternating tree automaton, and a trace log obtained from some given clause set S, and checks whether the clauses in S all hold in the model M. This is a way of getting confident that there is indeed no proof of the initial query, i.e., that your query is wrong. More useful is the fact that `h1mc` can give you an explanation, based on M, why you query is wrong. As with `h1trace`, this explanation can be made for humans, in text format, or in Coq format, to be checked independently by the Coq proof assistant. This is important in security protocols for instance, where a proof of secrecy consists in showing that there is no proof of the fact that the intruder can get hold of a given secret. This was shown by [2001 (Selinger)], see [2004 (Goubault-Larrecq)]. Adding `h1mc` gives you the following picture of the `h1` tool suite.
The `h1mc` tool is described in Section 6.
Additionally, various tools are provided. First, there are two conversion utilities, `auto2pl`, which converts deterministic tree automata in XML format into Prolog format (Section 8); and `pl2tptp`, which converts alternating tree automata in Prolog format into TPTP format (Section 10). Since every deterministic tree automaton is a particular case of an alternating tree automaton, and every alternating tree automaton is a particular case of an H1 clause set (see Section 2), these two utilities entail no loss of information. In particular, to convert deterministic tree automata into H1 clause sets, just run `auto2pl` on the former, getting an intermediate file which you then convert to H1 clause sets using `pl2tptp`.
Then, there are miscellaneous utilities. The first, `plpurge`, extracts the part of a tree automaton that is relevant to certain final states. In other words, it reads a tree automaton in Prolog format, and eliminates all states and transitions that do not reach any final state. This cleaning step is useful to help understand the structure of automata computed by `h1`, in particular as a preparation to calling `pl2gastex`. The `plpurge` tool is described in Section 9. The second, `tptpmorph`, applies certain kinds of morphisms to languages represented as H1 clause sets. This is described in Section 11. The need for it should become apparent in conjunction with `linauto`, which implements [1996 (Boudet and Comon)]'s algorithm for deciding quantifier-free Presburger formulae by converting them to automata. While `linauto` only deals with quantifier-free formulae, existential quantification can be dealt with by using `tptpmorph`, and universal quantification can be implemented using existential quantification and complementation. Complementation can be implemented by determinization (using `pldet`) and using `auto2pl` with the `-negate` option. The `linauto` tool is described in Section 12.
Finally, `pl2gastex` is a utility that converts alternating tree automata to a sequence of gasTEX macros, which can then be used in conjunction with LATEX to display them on screen or include them in documents. A former attempt of a tree automaton visualizer is provided with `autodot`. The latter converts deterministic tree automata to files in `dot` format; `dot` can then be applied to these files to display them graphically. This is only useful for relatively small automata, and is far from perfect for tree automata that are not just word automata. Don't expect too much from `pl2gastex` and `autodot` on anything else but small automata. The `autodot` utility is obsolescent: basically, it never gives satisfying output. The `pl2gastex` utility is more satisfactory, but not perfect. See Section 13.
At this point the picture of the `h1` tool suite is complete—up to the fact that I did not talk about some minor extensions yet, and that more extensions may be added in the future.