lanxicy.com

第一范文网 文档专家

第一范文网 文档专家

http://www.lsv.ens?cachan.fr/Publis/

In Proc. 10th Int. Conf. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’2003), Almaty, Kazakhstan, Sep. 2003. volume 2850 of Lecture Notes in Artificial Intelligence, pages 183?195. Springer, 2003.

On Closure under Complementation of Equational Tree Automata for Theories Extending AC

Kumar Neeraj Verma

LSV/CNRS UMR 8643 & INRIA Futurs projet SECSI & ENS Cachan, France verma@lsv.ens-cachan.fr

Abstract. We study the problem of closure under complementation of languages accepted by one-way and two-way tree automata modulo equational theories. We ? ), idempotent deal with the equational theories of commutative monoids ( ?? ), Abelian groups ( ?? ), and the theories of commutative monoids ( ? ), generalized exclusive-or ( ? ? ), and distributive miexclusive-or ( nus symbol ( ? ). While the one-way automata for all these theories are known to be closed under intersection, the situation is strikingly different for ? and ? automata are closed complementation. We show that one-way under complementation, but one-way ? , ? ? , ?? and ?? automata are not. The same results hold for the two-way automata, except for the ?? , as the two-way automata modulo all these theories except ?? theory are known to be as expressive as the one-way automata. The question of closure ?? automata is open. under intersection and complementation of two-way

1

Introduction

Tree automata [4, 2] enjoy many good properties: emptiness is decidable, the class of languages accepted is closed under Boolean operations notably. Two-way tree automata extend ordinary tree automata (call them one-way tree automata to distinguish them from two-way tree automata) by allowing transitions that not only construct terms, as in one-way automata, but also destruct terms (see [2], Chapter 7, Alternating Tree Automata). More speci?cally, one-way automata have transitions of the form “if terms ?? ?? are accepted at states ?? ?? then term ??? ?? ? is accepted at state ?”. The new transitions allowed in two-way automata are of the form “if term ??? ?? ? ? is accepted at state ? and terms ? ? ? are accepted at states ?? ?? then term ? is accepted at state ? ? ” where ? ?. Two-way tree automata are more ? conveniently represented by the so called de?nite clauses of ?rst order logic which provide a uniform mechanism for representing various kinds of transitions, like alternation (“if term ? is accepted at states ?? and ?? then ? is accepted at state ? ”), transitions with equality constraints between subterms, etc. Two-way tree automata can be effectively reduced to one-way tree automata. As a result they also enjoy the good properties of decidability of emptiness and closure under Boolean operations.

Partially supported by the ACI “cryptologie” PSI-Robuste, ACI VERNAM, the RNTL project EVA and the ACI jeunes chercheurs “S? curit? informatique, protocoles cryptographiques et e e d? tection d’intrusions”. e

? · ?? · ?? ?? · ?? · ? ?·? ?·? ?·? ? The extensions of ? that we deal with are obtained by adding one of the following ?: axioms to the base theory ( ) ? · ? ? (xor axiom) ( ?) ? · ?? · ? ? (generalization of xor axiom, where ? ?)

( ) ( ) (? ) (? ) ( ) (? )

? times

In spite of having the same expressiveness as one-way automata, two-way automata are sometimes more convenient to work with because of the new kinds of transitions. An important area in which two-way tree automata have recently been applied is veri?cation of cryptographic protocols [11, 6], where terms are used to represent messages and tree languages to represent sets of messages known to an intruder. The transitions of two-way tree automata allow us to model the ability of the intruder to encrypt and decrypt messages. This approach works ?ne when the cryptographic primitives are assumed to be perfect, in which case the messages are the members of the free term algebra. However often complex cryptographic primitives have additional algebraic properties, which need to be modeled using equational theories. The theory of associativity and commutativity, and its extensions like the theories of exclusive-or and Abelian groups are some examples that occur often. As an example the original version of the Bull’s recursive authentication protocol presented in [14] was formally proved correct using the assumption of perfect cryptographic primitives. However this protocol uses the exclusive-or operation for encryption. By taking into account the properties of the exclusive-or operation, an attack against this protocol was found in [15]. Also protocols like the group Dif?e-Hellman protocol [16], use algebraic properties of modular exponentiation [3]. This motivates exploring variants of tree automata which take into account equational properties of the function symbols. Several notions of tree automata accepting terms modulo equational theories have been proposed recently [9, 12, 18], which extend the tree automata concept. The notions of one-way and two-way equational tree automata have been studied extensively in [18] which deals with several variants of the equational theory ? of an associative, commutative operator · with unit ?. It shows the decidability of emptiness and closure under intersection of the one-way automata for all these theories, as well as the equivalence between two-way and one-way automata for most of these theories. However the problem of closure under complementation has been left open. In this paper we examine this question. More speci?cally, we study one-way and two-way equational tree automata, modulo the theory ? and several of its extensions. The theory ? of an associativecommutative symbol · with unit ? consists of the three axioms:

? · ???? ? (minus axiom) ??? · ?? ???? · ????, ????? ?, ?? ? (distributivity of ‘?’ symbol) ? · ? ? (idempotence) where ? is an additional unary symbol. We name a theory by the names of its axioms; e.g., ?? is the theory of Abelian groups and ? the theory of xor. Note that

is implied by ?? , so ? is a (strictly) weaker theory than ?? . The theories dealt with in this paper are ? , ? , ? ?, ? , ?? and ?? . ? and ? the one-way automata are closed unWe show that modulo der complementation. On the other hand, modulo ?? , ?? (Abelian groups), ? (the theory of xor) and ? ? , the one-way automata are not closed under ?? , the same results hold for two-way tree complementation. Except for the theory automata. The case of two-way ?? automata is open. An interesting pattern visible here is the coincidence between closure under complementation of the one-way equational tree automata and the linearity of the equational theory involved. These results on complementation are in sharp contrast to the results on intersection. Plan. After some material on related work, we de?ne our one-way and two-way equational tree automata in Section 2, recalling some important results, notably connections of ? automata with semilinear sets. These results are used in Section 3 to show closure under complementation of (one-way and two-way) ? automata. The (one-way and two-way) ? and ? ? automata are not closed under complementation, ? and Abelian groups case, we ?rst genas shown in Section 4. To deal with the eralize the results of Section 1 on ? automata to the ? case in Section 5. These are then used to show closure under complementation of (one-way and twoway) ? automata in Section 6. The results and proofs in the Abelian groups case ?? ) are exactly as in the ? case, as we argue in Section 7. Lastly we show ( that the one-way ?? automata are not closed under complementation in Section 8, ?? automata. We conclude in Section 9. leaving open the question for two-way Related work. Tree automata modulo have been considered several times, though not all these notions coincide. Lugiez [9] considers one-way AC tree automata which have additional sort restrictions, but are also extended with a rich constraints language. Recent work by Lugiez [10] extends it to include equality and counting constraints, providing a rich framework that includes most known proposals for one-way tree automata with decidable emptiness problems. The resulting class of automata is also shown to be closed under Boolean operations. This framework is however incomparable to ours: while Lugiez’s automata accommodate equality tests naturally, our two-way automata cannot avoid undecidability in the presence of equality constraints [7, 18]. Ohsaki [12, 13] considers a larger framework of (one-way) tree automata, where is an equational theory. Ohsaki’s regular automata coincide with our one-way tree automata when is linear (like , ? ), but this does not hold in theories like ? , ?? , ?? . For example, in Ohsaki’s case, with transition rules ?, ? and ? ?? , and with the theory ? , we have · ? ?? , meaning · is accepted at ? ? . In our case, with the corresponding clauses ? ? ?, ? ? ? and ? ? ???, and ? , · is not accepted at ?? . For arbitrary we do not know with the theory the relation between our automata and Ohsaki’s automata, and the two notions appear rather dissimilar. One of the key differences is that while we extend the traditional correspondence between tree automata and logic programs from the non-equational case to the equational case, Ohaski’s automata do not preserve this correspondence, as they mix equality on terms with equality on states, as illustrated by the above example.

While we consider tree automata as logic programs and extend them by adding equational theories, there has also been much work on equational logic programs [8] as such, which are logic programs in which the special equality predicate also appears, so that the equational theory can be coded in the logic program itself. In this context, complementation of equational tree automata corresponds to negation in equational logic programs. However our equational tree automata differ in that the equality symbol does not occur in the logic programs, and we separately consider an equational theory in which the equality predicate occurs. Moreover the author is not aware of any work on ?nding decision procedures or closure properties for subclasses of equational logic programs, especially for the ones corresponding to our automata. The notion of two-way equational tree automata has been studied by GoubaultLarrecq and the author [7, 18] for the theory and its variants. Note that the speci?c theories ? , ?? , etc., that we consider have traditionally not been considered in the framework of (one-way) tree automata; they give rise to speci?c technical problems and solutions. The notion of alternating two-way tree automata is treated in detail in [7], which also considers some additional push clause formats which are not relevant in this paper. Finally we have found that closure under Boolean operations has also been shown for the multiset automata of Colcombet [1], which correspond to the subclass of our one-way ? automata in which all symbols other than · ? are unary, and were introduced for studying process rewrite systems. To avoid confusion we clarify that the “two-way automata” of [17] are an entirely different notion from ours.

2

Two-Way -Tree Automata

Fix a signature ? of function symbols, each coming with a ?xed arity, and let be an equational theory, inducing a congruence on the terms built from ? . We will use clauses of ?rst order logic as a general means of representing various classes of automata. A de?nite clause is an implication of the ? ??? ? ?? ??? ? ?? ??? ? (1) form: where ? ?? ?? are predicates and ? ?? ?? are terms built from ? and variables. Given a ?nite set of such de?nite clauses we de?ne derivations of ground atoms using the following two rules: where is a ground substitution. Thus a derivation is a tree-like structure, which should not be confused with the trees which are the terms built from ? . Accordingly, a subderivation of a derivation ? is a subtree of ? . The last step of a derivation ? refers to the step at the root of ? . The connection of de?nite clauses with automata is as follows: predicates are states, ?nite sets of de?nite clauses are automata, and an atom ? ??? is derivable using , iff the term ? is accepted at state ? in the automaton . The derivations using are sometimes called runs of the automaton . It is also easy to see that the set of derivable atoms is exactly the least Herbrand model of the set of clauses modulo . ? is the set of terms ? such that ? ??? is derivable. When The language ?? ? is the empty theory, we shall call it ?? ? ?. If in addition some state ? is speci?ed

?? ??? ? ?? ??? ? if ? ??? ? ?? ??? ? ? ?? ? ?? ??? ? ? ? ?×? ? ??? if × ?

as being ?nal then the language accepted by is ?? ? ?? ? ?. Also, given a language ? and an equational theory , ??? denotes the set of terms ? such that ? × for some × ? ?. We de?ne one-way automata as consisting of clauses: (2) (3) which we shall call pop clauses and epsilon clauses respectively. In (2), the variables ?? ?? are distinct. These automata (without equations) are exactly the classical tree automata usually described in the literature. It may be helpful to read the pop clause as: “if terms ?? ,...,?? are accepted at states ?? ,...,?? respectively, then ??? ?? ? is accepted at ? ”. This is usually denoted by the rewrite rule ??? ?? ? ? . The epsilon clause corresponds to the rewrite rule ?? ? . We have the following easy result: Lemma 1 ([18]). For any one-way automaton ??? ? ??. In particular emptiness of one-way and equational theory , ?? ? tree-automata is decidable.

?

? ? ???

?? ?? ? ?? ??? ?

?? ???? ? ??? ? ?? ???

For Ohsaki’s regular tree automata, this result holds if is linear, but not in general. A counter-example is the automaton modulo ? given in Section 1. Since we are dealing with theories extending ? , we assume that ? contains symbols ·, ? and in presence of equations or ? the symbol ?. Note that we don’t consider the case of ? containing several · (resp. ?, ?) symbols. Symbols in ? ? ? · ? ? , are called free. Free symbols of zero arity are called constants. Terms of ?? ? where is free are called functional terms. Accordingly the pop the form ??? clauses in our automata are of the following form:

? ?? · ?? ? ?? ??? ?? ??? (4) ? ??? (5) ? ? ??? ?? ?? ? ?? ??? ?

??

? where

is a constant ? ???? ? ?? ??? being free

(6) (7) (8)

?? ??? ?

Clauses (6) are special cases of clauses (8). One-way ? (resp. ?? , ? , ? ? ) automata are sets of clauses (3), (4–6) and (8); one-way ?? and ? automata in addition contain clauses (7). We de?ne two-way automata by adding the following kind of clauses

??? ? ? ? ? ??? being free, ? ? ?

?

?? ?? ?? ?? ? ?

?

? ??

?

?

?

?

(9)

called push clauses, to one-way automata (the variables ?? ?? are distinct.) Hence two-way automata are sets of clauses (3) and (4–9)—with the proviso that (7) is only included when ? ? ? . The side-conditions “ ? ? ? ? ? ? ? ?” have been introduced in clause (9) to avoid undecidability problems. This is discussed in [18], which also argues that removing the side-condition “ being free” from clause (9) has no impact in the case of theories ? and ?? but is prob? and ? . Hence, while the expreslematic in the case of other theories like sion “two-way automata” is normally used in a general sense, without the restrictions

imposed by the side-conditions in clause (9), however in the rest of this paper, this expression will be used in the specialized sense de?ned above. Constant-only automata are one-way automata which contain clauses (6) instead of the general clauses (8) (the only free symbols in the signature are constants.) Given a one-way or two-way automaton , we de?ne ? to be the part of with clauses (3), (4), (5) and (7) (the equational part), and ? is the remaining part. Example 1. Consider a signature having constants and , a unary symbol and a binary symbol . De?ne two-way automaton modulo ? to consist of the clauses (i) ?? ? ? (vi) ? ?? · ? ? ? ?? ??? ?? ?? ? (ii) ?? ? ? (vii) ? ?? · ? ? ? ? ??? ?? ?? ? (iii) ?? ? ???? ? ?? ??? (viii) ? ??? ? ? ? ?? ? ?? ? ?? ? (iv) ? ??? (ix) ? ?? · ? ? ? ? ??? ?? ?? ? (v) ? ? ?? ? ?? ? ? ??? ?? ?? ? Then the following is an example of a derivation in the automaton. At each step, the clause applied or the equational rewriting used is indicated on the right side.

??

? ??? ??

? ?? ??

?? ?

?? ? ?

? ? ? ?? ? ?

?? ?

??

?

?? ?

?? ? ?

? ? ? ?? ? ?

? ??

? ??

? ???

· ? ??

?? ?

?

?

??

? ???

? ???

??

· ? ?? · ?? ? ?? ??

?? ?

?ACUX?

? ?? · ? ?ACUX? ???

?? ?

?

??

? ??

The languages accepted by all our one-way or two-way automata are trivially closed under union. It has been shown in [18] that the one-way automata for all these theories ( ? , ? , ? , ? ? , ?? , ?? ) are closed under intersection. There it is also shown that two-way automata are as expressive as one-way automata, for all these theories, except ?? for which the problem is currently open. The emptiness test for one-way automata has already been dealt with (Lemma 1). In this paper, we shall concentrate on closure under complementation of these automata. Note also that closure under intersection and decidability of emptiness imply decidability of membership of one-way equational tree automata for all theories considered in this paper since, using Lemma 1, for any theory and term ?, the language ? ? ? is easily recognized by a one-way tree automaton. First we recall some important results on constant-only ? automata. Let the ? , the ground terms are of the constants in our signature be ? ? . Modulo ? form with ? ? ? : equivalently ?-tuples of natural numbers. Recall that a ?? linear set is a set of the form · ?? ? · · ? ?? ? ? ? for some ? ? ? . A semilinear set is a ?nite union of linear sets. The semilinear sets ? are exactly the sets de?nable in Presburger arithmetic [5]. In particular they are closed under union, intersection, complementation and projection. Then we have:

?

Lemma 2 ([18]). Constant-only

allows us to ‘reuse’ parts of derivations. This will be required very often in the paper.

? automata accept exactly semilinear sets. To prepare ourselves, we need another special property of ? automata which

? . Consider a derivation Lemma 3 ([18]). Let be any set of equations containing ? of an atom ? ??? modulo . Let ?? ?? be non-overlapping subderivations of ? such that outside the ? ’s, the only equations used are ? and the set ? of clauses used contains only clauses of kind (3), (4) and (5) (see Figure 1, noting that the derivation ?? are trees are shown with the root at the top.) Suppose the conclusions of ?? ?? ??? ? ?? ??? ?. Then

1. ? ? ?? · · ? ? ? ? ?? of atoms ?? ?×? ? ???×? ? modulo then there 2. If there are derivations ?? ? of ? ?×? · · ×? ? modulo , containing ?? ’s as subderivations, is a derivation ? ? , and all clauses used such that outside the ? ? ’s, the only equations used are belong to ? .

? ??? ·

· ?? ?

? ?×? ·

· ×? ?

clauses (3), (4) modulo

clauses (3), (4) modulo

?

... ?? ???

? ?? ???

...

?? ??? ? ??

...

?? ??? ? ??

? ???

?? ?×? ? ??

?

...

?? ?×? ? ??

?

? ???

Fig. 1. Reuse of

? derivations

The following de?nition gives one way of computing such ? ’s and ? ?? ?’s:

De?nition 1. Consider a derivation ? of an atom ? ??? in a one-way automaton modulo ? . Let ?? ?? be the set of maximal subderivations of ? in which the last step used is an application of clause (8) (or clause (6)). Suppose the conclusions of ?? ?? are ?? ??? ? ?? ??? ? (in which case ?? ?? must be functional.) Then we will say that the (unordered) list of atoms ?? ??? ? ????? ? is the functional support of the derivation ?. (From Lemma 3 we have ? ? ?? · · ?? .)

3

Complementation of

? Automata

Let be a one-way ? automaton with predicates from some ?nite set ?. We introduce new predicate symbols ? and ? for each ? ? and constants ? for each ? ? . We intend ? to accept terms accepted at all the predicates in ? but nowhere else. ? is intended to accept the functional terms accepted at ? . De?ne automaton ?? ? ? ? ? ? ? ? . The idea in de?ning ? is to ? compute all possible derivations using the clauses of the equational part. The constant ? acts as abstraction for the terms accepted at ? for ? ? .

? ? is a semilinear set for every ? ? ?. Given ? ?, From Lemma 2, ?? ? ?? ?? ? ? ? ? ? ???? ?? ? ?? ? ?. This is a semilinear set. de?ne ? ? ?? ?? ? By Lemma 2, we can construct a constant-only automaton ? with ?nal state ? such that ?? ? ? ? ?? . We assume that automata ? ’s are built from mutually disjoint sets of (fresh) states. De?ne automaton ? to consist of the following clauses:

?

?

– – – –

for each ? ? the clause ? ??? ? ? ???. clauses (3), (4) and (5) (but not (6)) from each ? . for each clause ?? ? ? in some ? , the clause ???? ? ? ???. for each free function symbol of arity ?, and each ?? ? ? ??? ?? ?? ? ?? ??? ? ?? ??? ? where ? ? ?? ? ? ??? ?? ?? ? ?? ??? ? ?? ??? ? ? ? .

?? ?, the clause ? ? ? ?? ? ? ?

This construction plays the role of the usual determinization procedure in standard tree automata. Note that it is however more complex because of the ? symbol. We have the following result:

? and any term ?, ? ??? is derivable in Lemma 4. For any ? ? ? ? ? ? ??? is derivable in modulo ? .

? modulo

? iff

?? where for ? Proof. By induction on the size of ?. Let ? ? ?? · · ?? ?? ? ?, for some free . Let ? ? ? ? ? ??? is derivable in . ?, ? ??? First we show that (a) ? ??? is derivable in ? modulo ? ; then we show that (b) if ? ? ??? is derivable in ? modulo ? for some ? ? ? then ? ? ? . Proof of (a). For ? ?? let ? ? ??? ? is derivable in modulo ? . By induction hypothesis ? ?? ? is derivable in ? modulo ? . For ? ? let ? ? ?? ? ? ? ? ? ? ?? ??? ? ?? ? ?? ?? ? ? ?? ? ? . Then the clause ? ? ??? ? ?? ? ? ? ??? ? ? ?? ? ? ?. So ? ?? ? is derivable in ? modulo ? for ? ?. For each ? ? ? , the derivation of ? ??? has a functional support of the form ?? ??? ? ?? ??? ?. For ? ? ? ? ?, the derivation of ?? ?? ? uses at the ? ? ?? ? ? ?? last step, a clause ? ? ?? ? ? ??? ? ?? ?? ? and derivations ? ? ? of ? ?? ??? ?. Then ? ? ? for ? ? ? ? ?? . Hence ?? ? ? . By Lemma 3, (*) ? ? ?? · · ?? ? is derivable in ?? modulo ? for each ? ? ? . (**) If ? ? ? ? ? then ?? · · ?? ? ?? ? ?? ? ?. Otherwise the corresponding derivation would have a functional support of the form ?? ? ?? ? ? ? ? ?? ? where ? ? ? for ? ?. Then by construction of ? , ? ?? ? would be derivable for ? ?. Then by Lemma 3, ? ??? · · ?? ? would be derivable in modulo ? . Hence we would have a derivation of ? ??? in modulo ? which contradicts the de?nition of ? . Combining (*) and (**), ?? · · ?? ? ?? . The derivation of ? ? ?? · · ?? ? in ? modulo ? has a functional support of the form ?? ? ?? ? ?? ? ?? ?. Then ? ?? ? is derivable in ? modulo ? using the clause ? ??? ? ? ??? for ? ?. Hence by Lemma 3 we get a derivation of ? ??? · · ?? ? in ? modulo ? . Finally

we use the clause ? ??? ? ? ??? to get a derivation of ? ??? · · ?? ?, i.e. of ? ???. This proves (a). Proof of (b). Now suppose ? ? ? such that ? ? ??? is derivable in ? modulo ?. ? . The derivation of ? ? ??? uses at the last step a derivation of We show that ? ? ? ? ? ???. From the construction of , the latter derivation has a functional support of ? ??? ? ?? ??? ? and the clauses used immediately above the derivation of ? the form ?? ? ? ?? ? are of the form ?? ??? ? ? ? ??? corresponding to the clause ?? ? ?? ? of ?? . Also

the clauses used above the clauses ?? ??? ? ? ? ??? are from ? ? . Then by Lemma 3, ? ? ? . For ? ? the derivation ? ? ? ?? · · ?? ? is derivable in ? ? modulo ? ?? ? uses at the last step a clause of the form ? ? ? ??? ? ?? ? ? ?? ??? ? of ? ?. Then by induction hypothesis ? ? ?? ? ? ? and derivations of ? ? ?? ??? ? ? . Then by de?nition of ? , ? ? ? . Hence ? ?? · · ?? ? ?? ? . We have ? . Since the ?? ’s are mutually disjoint, so ? ? ? . already seen that ?? · · ?? ? ?

? ?

As a consequence we obtain: Theorem 1. One-way

Proof. Let . De?ne automaton ? as above. Pick a new predicate ? . Add to ? the clauses ? ??? ? ? ??? for every ? ? ? ? . Call this new automaton ?. Then by ? Lemma 4, ? ? ? ? ? ? ? iff for some ? ? ? ? we have ? ? ?? ? ? ? ?, iff ? ? ? ? ? ? ?? ? ? ? iff ? ? ? ? ? ?. Hence ? accepts the complement of the language accepted by . ? ? Since two-way ? automata have the same expressiveness [18] as one-way automata, we also have: Theorem 2. Two-way

? automata are closed under complementation. be a one-way ? automaton with predicates from ? and with ?nal state

?

? automata are closed under complementation.

The idea of using constants as abstractions for the functional terms accepted at certain states, and the correspondence between constant-only ? automata and Presburger de?nability, have already been used in [18] to show closure under intersection of various classes of automata. This may give the impression that the arguments for closure under complementation are similar to the ones for intersection. There are indeed some common ideas, which led the author to conjecture that one-way tree automata modulo all theories considered here are closed under complementation. However it was surprisingly found that while these ideas work for showing closure under intersection of the one-way automata modulo all theories under consideration, they don’t work for showing closure under complementation of the one-way automata modulo the theories ? , ? ?, ?? and ?? . We will show that the latter are not closed under complementation. Unlike in the case of intersection, our results show a strong correlation between closure under complementation of one-way equational tree automata and the linearity of the equational theory involved, at least as far as the theories dealt with in this paper are concerned.

4

Counter-Example for

Contrary to the ? case, ? automata are not closed under complementation, as we show in this section. The result generalizes to the ? ? case for ? ?, i.e. we can show that one-way or two-way ? ? automata are not closed under ? case by making ? ?.) To show complementation for any ? ?. (We get the ?? ? · ? · ?? ? ? this ?x some ? ?. De?ne languages ?? ? (assuming a signature that has at least a unary symbol and a constant ) and ?? ? . ? ?, so that, for example, Let us clarify that we are considering languages modulo when we write ? , we actually mean the language ? ? ? ? ? . Similar remarks ?? ? · · ?? ? hold for other theories considered later. Then ?? ? ?? ? and for some ? ? and . ?? and ?? are clearly ? ? ? ? automata. However ?? ? ?? is not: accepted by one-way

? ? ?· · ?? ? Lemma 5. The language ? ? ? and is not accepted by any one-way ?

?

and

?

? Automata

?

? and for some ? ? automaton.

Proof. Assume on the contrary that there is a one-way automaton with ?nal state ? which modulo ? ? accepts ?. Let ? be the set of predicates in . For each ? ? de?ne ?? ? ? ? ?? ? ? ?? is derivable in modulo ? ? . Since ? is ?nite, it has ?nitely many subsets. Hence we have some ? ? such that ?? ?? . Since ? ?, the term ? ? ? · ???? ? ? ? ? ?. From Lemma 1, we have some ? ? ? · ??? ? ? ? such that ? ??? is derivable in modulo ? ? . We ? ? ? ?? · ?? · · ?? · ?? · · ?? · · ?? · · ?? ? ?? such that ? have ? ? ? ? ?? ? and ? are functional for ? ? ?, ?? ? ? ? ? ?, ? ? ? ? ? ?. The derivation of for ? ?, and ? ? ? ? ? for ? ? ? ? ??? has functional support of the form ?? ??? ? ????? ? ?? ??? ? ?? ??? ? ?? ??? ? ? ? ? ??? ? ? ??? ?. Then ? ? ? and ? ? ? ?? ? ?? . However ?? ?? , hence ? ? ? ?? ?? ? ?? . Thus ?? ? ? ? ??? ??? ? ? ?? ??? ? ? ?? are derivable in modulo ? ? . By Lemma 3, ? ? ? ? ? ? · ?? · · ?? · · ?? · · ?? ? (or ? ???) ? ? is derivable in modulo ? ? leading to contradiction. ? ?

?

?

?

Theorem 3. One-way ? ? automata are not closed under complementation for ? automata in particular. any ? ?. This holds for one-way The key idea, also used in the further counter-examples, is that in presence of nonlinear equations like , doing complementation involves putting disequality constraints on subterms, which is beyond the power of our automata. Again, since two-way ? ? automata have the same expressiveness [18] as oneway ? ? automata, we get:

Since ?? ? ??

??

???? ? where ???? ? denotes the complement of ?? , we have:

Theorem 4. Two-way ? ? automata are not closed under complementation for any ? ?. This holds for one-way ? automata in particular.

We remark that the situation is different for the theory ? ? when ? ?. In this ? means that every term is equal to ?. Trivially the automata are case the axiom ? closed under intersection and complementation. This is clearly not an interesting case.

5

Constant-Only Derivations

?

Automata and Reuse of

?

In this section we generalize Lemmas 2 and 3 to the ? case. These will be useful ? and ?? automata. in dealing with the First we consider constant only ? automata. Recall that ? is the set of con? ? . Terms built stants in our signature. Let ? be a set of fresh constants from ? · ? ? modulo ? are of the form ? · · ? ? ? ? ? ? (? ? ?) while those built from ? ? · ? modulo ? are of the form · · ? · ? · · ? (? ? ?). Hence there is a natural 1-1 correspondence ? between terms (languages) on ? · ? ? modulo ? and terms (languages) on ? ? · ? modulo ? . Then modulo this correspondence of languages:

? automata with Lemma 6 ([18]). The language accepted by a constant-only constants from ? is a semilinear set with constants from ? ? . Conversely, a semilinear set with constants from ? ? can be represented as accepted by a constant? automaton with constants from ? . only

Also we have the following generalization of Lemma 3 to the

?

case.

? . Consider a derivation ? Lemma 7. Let be any set of equations implying of an atom ? ??? modulo . Let ?? ?? be non-overlapping subderivations of ? such that outside the ? ’s, the only equations used are ? and the set ? of clauses used contains only clauses of kind (3), (4), (5) and (7). Suppose the conclusions of ?? ?? are ?? ??? ? ????? ?. Then

1. ? ?? ? · ? . (·?? means ?? .) ? ?? ?? ?? ?? ?? for some ?? ? ? ?? of atoms ?? ?×? ? ???×? ? modulo then there 2. If there are derivations ?? is a derivation ? ? of ? ??? ×? ?? ?? ×? ? (the ? ’s here are the same as above) modulo , containing ? ? ’s as subderivations, such that outside the ? ? ’s, the only equations used are ? , and all clauses used belong to ? . Finally the notion of functional support is generalized to

?

derivations.

De?nition 2. Consider a derivation ? of an atom ? ??? in a one-way automaton modulo ? . Let ?? ?? be the set of maximal subderivations of ? in which the last step ?? used is an application of clause (8) (or clause (6)). Suppose the conclusions of ?? are ?? ??? ? ?? ??? ? (in which case ?? ?? must be functional.) Then we will say that the (unordered) list of atoms ?? ??? ? ?? ???? is the functional support of the derivation ? . (From Lemma 7, ? must be of the form ?? ?? ?? ?? ?? .)

6

Complementation of

?

Automata

In the ? case the situation is similar to the ? case: the automata are closed ? case, we give the full under complementation. The arguments being similar to the construction with a sketch of the proof.

Let be a one-way ? automaton with predicates from ?. Introduce predicate symbols ? and ? for each ? ? , and sets of constants ? ? ? and ? ? . De?ne automaton ?? ? ? ? ? ? ? ? . From ? ? ? ? is a semilinear set on constants from . Lemma 6, for each ? , ?? ? ?? Given ? ? , de?ne ?? ?? ? ?? ? ? ? ? ???? ?? ? ?? ? ?. This ? ?? is a semilinear set on constants from . By Lemma 6 we can construct a constantonly ? automaton ? , using constants from , and with ?nal state ? such that ?? ? ? ? ?? . We assume that automata ? ’s are all built from mutually disjoint sets of (fresh) predicates. De?ne automaton ? to consist of the following clauses:

?

?

– – – –

for each ? ? the clause ? ??? ? ? ???. clauses (3), (4), (5) and (7) (but not (6)) from each ? . for each clause ?? ? ? in some ? , the clause ???? ? ? ???. for each free functional symbol of arity ?, and each ?? ? ? ??? ?? ?? ? ?? ??? ? ?? ??? ? where ? ? ?? ? ? ??? ?? ?? ? ?? ??? ? ?? ??? ? ? ? .

?? ?, the clause ? ? ? ?? ? ? ?

? modulo

? and any term ?, ? ??? is derivable in Lemma 8. For any ? ? ? ? ? ? ??? is derivable in modulo ? .

?

iff

Proof. By induction on the size of ?. Let ? ? ×? · · ×? ??? ? ??? ?? ? ?? where for ? ?× ?×? × ? for some free , and for ? ? ? ??? ?? ? for some free . Let ? ? ? ? ? ??? is derivable in . First we show that (a) ? ??? is derivable in ? modulo ? ; then we show that (b) if ? ? ??? is ? modulo ? for ? ? ? then ? ? ? . derivable in Proof of (a). For ? ?? let ? ? ??× ? is derivable in modulo ? . By induction hypothesis ? ?× ? is derivable in ? modulo ? . ?? ? let ? ? ??? ? is derivable in modulo ? . For ? Then by induction hypothesis ? ?? ? is derivable in ? modulo ? . For ? ? ?? ? ? ? ? ? ? ?? ??? ? ?? ? ?? ?? ? ? let ? ? ?? ? ? . Then the clause ? ? ??? ? ?? ? ? ? ??? ? ? ?? ? ? ?. ? for ? So ? ?× ? is derivable in ?. Similarly for ? ? let ? ? ?? ??? ? ? . Then the ?? ? ? ? ?? ? ? ? ?? ??? ?? ?? ? ?? ?? ? ?? ?? ? ? ? ??? ? ? ? ??? ? ? ?. So ? ?? ? is derivable in ? clause ? ? ??? for ? ?. ? case, but using Lemma 7 instead of Lemma 3 we show that Arguing as in the ? ? ?? · · ?? ? ?? ? ? ?? ? is derivable in ?? modulo ? for each ? ? ? . ? ?. Also we show that if ? ? ? ?? then ?? · · ?? ? ?? ? ? ?? ? ?? ? ?? Hence ?? · · ?? ? ?? ? ? ?? ? ?? . The derivation of ? ? ?? · · ? ?? ? in modulo ? has a functional support of the form ?? ? ?? ? ? ? ?? ? ?? ? ??? ?? ? ?? ? ?? ? ?? ? ?? ?. As in the ? case we use Lemma 7 to get a derivation of ? ?×? · · ×? ? ?? ? ? ?? ? in ? modulo ? . Finally we use the clause ? ??? ? ? ??? to get a derivation of ? ?×? · · ×? ? ?? ? ? ?? ?, i.e. of ? ???. This proves (a).

? ?? ? ? ?? ??? ? ? ? ?? ? ? of ? ? ?× ? uses at the last step, a clause ? ? ? ??? ? ?× ??? ? ? and derivations of ? ?. By induction hypothesis ? ? . By de?nition of ? , ? ? ? . Similarly for ? ?, ? ? ? . Hence ?? · · ?? ? ? ?? ? ? ?? ? ?? ? . We have already seen that ?? · · ?? ? ?? ? ? ?? ? ? . Since the ?? ’s are mutually disjoint, we have ? ? ? . ? ?

Then as in the ? case, and using the fact that two-way ? automata have ? automata, we conclude: the same expressiveness [18] as one-way Theorem 5. One-way ? automata are closed under complementation. Also twoway ? automata are closed under complementation.

Proof of (b). Now suppose ? ? ? such that ? ? ??? is derivable in ? modulo ? . We show that ? ? ? . The derivation of ? ? ??? uses at the last step a derivation of ? ? ???. ? ? ?? ?×?? ??? ??? ? The latter derivation has a functional support of the form ?? ?×? ? ? ?? ??? ?. Arguing as in the ? case, we use Lemma 7 to show that ?? ? ??? · · ? ? ?? ? ? ? ?? ? is derivable in ?? modulo ? . For ? ? the derivation ?? ?

7

Counter-Example for

?? Automata

?? (Abelian groups theory) case is similar to the ? case. De?ne lan?? ? ? ?? ? ? ? ?? ? ? ?? ? , ?? ? . Then ?? ? ?? ? ? ? and ? ? is not accepted by any one-way ?? automaton: ?? ? ? ?? ? ? ? Lemma 9. The language ? ? and ? ? is not accepted by any one-way ?? automaton.

The guages ?? ? Proof. The proof is similar to that of Lemma 5, the difference being that we need the ? case (Lemma 7) instead of the ? case (Lemma 3). Assume on the contrary that there is a one-way automaton with ?nal state ? which modulo ?? accepts ?. Let ? be the set of predicates in . For each ? ? de?ne ?? ??? ?? ? ? ?? is derivable in modulo ?? . Then we have some ? ? such that ?? ?? . Then ? ? ? ? ? ? ? ? ?. We have some ? ?? ? ? ? ? ? ? ? such that ? ??? is derivable in modulo ? . ? ? ?? ? ?? · ?? ? ?? · · ? ? ? ? ?, ? ? ? ?, ? ? ?? such that ?? and ?? are functional, ?? ?? ? ?? ? ? are functional and ? . The derivation of ? ??? has ?? ? for ? functional support of the form ? ??? ? ? ??? ? ?? ??? ? ?? ??? ? ? ?? ? ? ?? ?. As before, ? ? ? ? ?? and ? ? ? ? ?? are derivable in modulo ?? . Then by Lemma 7, ? ? ? ? ? ? ?? ? · ?? ??? · · ? ?? ? (or ? ???) is derivable in modulo ?? leading to contradiction. ? ? Since one-way ?? automata are closed [18] under intersection and are as ex?? automata, we have as for the ? case: pressive [18] as two-way Theorem 6. One-way ?? automata are not closed under complementation. Nei?? automata closed under complementation. ther are two-way

8

Counter-Example for

?? Automata

?? ?

We now show that one-way ?? automata are not closed under complementation ?? ? · ?? ? ? ? ?? ? ? either. De?ne languages ?? ? and ?? ? ? ? · ? ? ? ? ? ? and ? ? . ? . We have ?? ? ?? Lemma 10. The language accepted by any one-way

?? ? · ? ?? automaton.

??

? and ?

?

is not

Proof. Assume on the contrary that there is a one-way automaton with ?nal state ? which accepts ?. Let ? be the set of predicates in . For each ? ? de?ne ?? ? ? ? ?? ? ? ?? is derivable in modulo ?? . We must have some ? ? such that ?? ?? . Then ? ? ? · ? ? ? ? ?. From Lemma 1, we must have some ? ? ? · ? ? ? such that ? ??? is derivable in modulo ? ?? ? . ? must be of the form ×? · · ×? · ?? · · ?? ?? ? ?? such that for ? ?? ?, × ? ? ? and ? ? ? ? . Then arguing as in the and ? are functional, × ?? ?? ? ? case, we get a derivation of ? ? ?·?? ? ? ?? (or ? ? ?? ??) modulo ?? leading to contradiction. ? ?

?

?? automata are closed [18] under intersection we have: Theorem 7. One-way ?? automata are not closed under complementation. ?? automata are closed unHowever this does not answer whether two-way

Since one-way

der complementation since the question of equivalence between two-way and one-way ?? automata is currently open [18]. Closure under intersection of two-way ?? automata is also left open in [18], but it is mentioned that the two-way ?? automata are powerful enough to encode alternation. This suggests that this case is dif?cult, because adding alternation to one-way automata is already known to produce undecidability in the case of theories ? ? ?? , while in the case of theories ? ? ?? the question is open.

9

Conclusion

We have studied the problem of closure under complementation of one-way and two? (associativity, commutativway tree automata modulo the equational theories ity, unit), ? ( ? with a distributive ‘?’ symbol), ?? (Abelian groups), ? (exclusive-or), ? ? (generalized exclusive-or), and ?? ( ? with idempotence.) We have shown that for the theories ? and ? , the one-way and two-way ?? , ? and automata are closed under complementation. For the theories ? ? , we have shown that neither one-way nor two-way automata are closed under complementation. In the case of ?? , while the one-way automata are not closed under complementation, the question in open for two-way automata. An interesting pattern visible here is the coincidence between closure under complementation of the one-way automata and the linearity of the equational theory.

These results are in sharp contrast with the results on closure under intersection. The one-way automata for all the above theories are known to be closed under intersection. Also, the two-way automata for all theories except ?? are known to be closed under ?? automata.) intersection. (The question is open for two-way The results about the two-way automata are obtained by reducing them to one-way automata. The equivalence between one-way and two-way ?? automata is however ?? automata are closed open. A positive answer would also mean that two-way under intersection but not under complementation. Acknowledgements: I thank Jean Goubault-Larrecq for discussions and suggestions, as well as the anonymous referees for helpful comments.

References

1. T. Colcombet. Rewriting in the partial algebra of typed terms modulo AC. In Electronic Notes in Theoretical Computer Science, volume 68. Elsevier Science Publishers, 2002. 2. H. Comon, M. Dauchet, R. Gilleron, F. Jacquemard, D. Lugiez, S. Tison, and M. Tommasi. Tree automata techniques and applications. www.grappa.univ-lille3.fr/tata, 1997. 3. W. Dif?e and M. Hellman. New directions in cryptography. IEEE Transactions on Information Theory, IT-22(6):644–654, 1976. 4. F. G? cseg and M. Steinby. Tree languages. In G. Rozenberg and A. Salomaa, editors, e Handbook of Formal Languages, volume 3, pages 1–68. Springer Verlag, 1997. 5. S. Ginsburg and E. H. Spanier. Semigroups, Presburger formulas and languages. Paci?c Journal of Mathematics, 16(2):285–296, 1966. 6. J. Goubault-Larrecq. A method for automatic cryptographic protocol veri?cation. In FMPPTA’2000, 15th IPDPS Workshops, pages 977–984. Springer-Verlag LNCS 1800, 2000. 7. J. Goubault-Larrecq and K. N. Verma. Alternating two-way AC-tree automata. In preparation. 8. M. Hanus. The integration of functions into logic programming: From theory to practice. Journal of Logic Programming, 19 & 20:583–628, 1994. 9. D. Lugiez. A good class of tree automata. Application to inductive theorem proving. In ICALP’98, pages 409–420. Springer-Verlag LNCS 1443, 1998. 10. D. Lugiez. Counting and equality constraints for multitree automata. In FOSSACS’03, pages 328–342. Springer-Verlag LNCS 2620, 2003. 11. D. Monniaux. Abstracting cryptographic protocols with tree automata. In SAS’99, pages 149–163. Springer-Verlag LNCS 1694, 1999. 12. H. Ohsaki. Beyond regularity: Equational tree automata for associative and commutative theories. In CSL’01, pages 539–553. Springer-Verlag LNCS 2142, 2001. 13. H. Ohsaki and T. Takai. Decidability and closure properties of equational tree languages. In RTA’02, pages 114–128. Springer-Verlag LNCS 2378, 2002. 14. L. C. Paulson. Mechanized proofs for a recursive authentication protocol. In 10th IEEE Computer Security Foundations Workshop, pages 84–95, 1997. 15. P. Ryan and S. Schneider. An attack on a recursive authentication protocol: A cautionary tale. Information Processing Letters, 65(1):7–10, 1998. 16. M. Steiner, G. Tsudik, and M. Waidner. Key agreement in dynamic peer groups. IEEE Transactions on Parallel and Distributed Systems, 11(8):769–780, 2000. 17. M. Y. Vardi. Reasoning about the past with two-way automata. In ICALP’98, pages 628–641. Springer Verlag LNCS 1443, 1998. 18. K. N. Verma. Two-way equational tree automata for AC-like theories: Decidability and closure properties. In RTA’03, pages 180–196. Springer Verlag LNCS 2706, 2003.

相关文章:

更多相关标签:

- Equational theories for inductive types
- ACTAS Automated Verification Based on Equational Tree Automata
- Equational theories for inductive types
- Combining Equational Tree Automata Over AC and ACI Theories
- On Closure Properties of Quantum Finite Automata
- Two-way equational tree automata for AC-like theories Decidability and closure properties
- Tree automata help one to solve equational formulae in AC-theories
- Minimum bases for equational theories of groups and rings The work of Alfred Tarski
- Combining Equational Tree Automata Over AC and ACI Theories
- Unification in the Union of Disjoint Equational Theories Combining Decision Procedures
- Extending the Tree-DOP Model with Grammatical Function Information 1 Background and motivat
- Extending Lustre with Timeout Automata Abstract
- Decidability and closure properties of equational tree languages
- ACTAS Automated Verification Based on Equational Tree Automata
- Definability in the lattice of equational theories of commutative semigroups