Alternating two-way AC-tree automata

9 years 1 months ago
Alternating two-way AC-tree automata
We explore the notion of alternating two-way tree automata modulo the theory of finitely many associative-commutative (AC) symbols. This was prompted by questions arising in cryptographic protocol verification, in particular in modeling group key agreement schemes based on Diffie-Hellman-like functions, where the emptiness question for intersections of such automata is fundamental. This also has independent interest. We show that the use of general push clauses, or of alternation, leads to undecidability, already in the case of one AC symbol, with only functions of arity zero. On the other hand, emptiness is decidable in the general case of several function symbols, including several AC symbols, provided push clauses are unconditional and intersection clauses are final. This class of automata is also shown to be closed under intersection. Key words: associative-commutative, tree automata, two-way tree automata, alternating tree automata, branching vector addition systems with stat...
Kumar Neeraj Verma, Jean Goubault-Larrecq
Added 14 Dec 2010
Updated 14 Dec 2010
Type Journal
Year 2007
Authors Kumar Neeraj Verma, Jean Goubault-Larrecq
Comments (0)