Paper Info
Title
Alternation in equational tree automata modulo XOR
Abstract
Equational tree automata accept terms modulo equational theories, and have been used to model algebraic properties of cryptographic primitives in security protocols. A serious limitation is posed by the fact that alternation leads to undecidability in case of theories like ACU and that of Abelian groups, whereas for other theories like XOR, the decidability question has remained open. In this paper, we give a positive answer to this open question by giving effective reductions of alternating general two-way XOR automata to equivalent one-way XOR automata in 3EXPTIME, which also means that they are closed under intersection but not under complementation. We also show that emptiness of these automata, which is needed for deciding secrecy, can be decided directly in 2EXPTIME, without translating them to one-way automata. A key technique we use is the study of Branching Vector Plus-Minimum Systems (BVPMS), which are a variant of VASS (Vector Addition Systems with States), and for which we prove a pumping lemma allowing us to compute their coverability set in EXPTIME.
Year
DOI
Venue
2004
10.1007/978-3-540-30538-5_43
FSTTCS
Keywords
Field
DocType
equational tree automata modulo,equivalent one-way xor automaton,general two-way xor automaton,equational tree,vector addition systems,open question,abelian group,one-way automaton,decidability question,equational theory,branching vector plus-minimum systems,security protocol
Abelian group,Discrete mathematics,Combinatorics,EXPTIME,Modulo,Computer science,Automaton,Decidability,Cryptographic primitive,Tree automaton,Pumping lemma for regular languages
Conference
Volume
ISSN
ISBN
3328
0302-9743
3-540-24058-6
Citations 
PageRank 
References 
3
0.46
18
Authors
1
Name
Order
Citations
PageRank
Kumar Neeraj Verma11718.87