Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2007 | 10.1016/j.ic.2006.12.006 | Inf. Comput. |
Keywords | Field | DocType |
associative-commutative,alternating tree automata,resolution,emptiness question,intersection clause,ac symbol,two-way tree automata modulo,tree automata,cryptographic protocols,two-way tree automata,general case,push clause,diffie-hellman-like function,branching vector addition systems with states,general push clause,cryptographic protocol verification,arity zero,cryptographic protocol,diffie hellman | Discrete mathematics,Automata theory,Combinatorics,Arity,Modulo,Symbol,Automaton,Decidability,Tree automaton,Mathematics,Alternation (linguistics) | Journal |
Volume | Issue | ISSN |
205 | 6 | Information and Computation |
Citations | PageRank | References |
6 | 0.47 | 52 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Kumar Neeraj Verma | 1 | 171 | 8.87 |
| Jean Goubault-Larrecq | 2 | 582 | 40.90 |