1 Introduction

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:

as deterministic bottom-up tree automata;
as alternating tree automata;
as pure Prolog programs (sets of Horn clauses) in the H₁ 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, H₁ 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 H₁ 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 H₁ clause set (see Section 2), these two utilities entail no loss of information. In particular, to convert deterministic tree automata into H₁ clause sets, just run auto2pl on the former, getting an intermediate file which you then convert to H₁ 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 H₁ 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 gasT_EX macros, which can then be used in conjunction with L^AT_EX 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.