TY - GEN
T1 - Extending H 1-clauses with path disequalities
AU - Seidl, Helmut
AU - Reuß, Andreas
PY - 2012
Y1 - 2012
N2 - We extend H 1-clauses with disequalities between paths. This extension allows conveniently to reason about freshness of keys or nonces, as well as about more intricate properties such as that a voter may deliver at most one vote. We show that the extended clauses can be normalized into an equivalent tree automaton with path disequalities and therefore conclude that satisfiability of conjunctive queries to predicates defined by such clauses is decidable.
AB - We extend H 1-clauses with disequalities between paths. This extension allows conveniently to reason about freshness of keys or nonces, as well as about more intricate properties such as that a voter may deliver at most one vote. We show that the extended clauses can be normalized into an equivalent tree automaton with path disequalities and therefore conclude that satisfiability of conjunctive queries to predicates defined by such clauses is decidable.
UR - http://www.scopus.com/inward/record.url?scp=84859151114&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-28729-9_11
DO - 10.1007/978-3-642-28729-9_11
M3 - Conference contribution
AN - SCOPUS:84859151114
SN - 9783642287282
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 165
EP - 179
BT - Foundations of Software Science and Computational Structures - 15th Int. Conf., FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Proceedings
T2 - 15th International Conference on Foundations of Software Science and Computational Structures, FOSSACS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012
Y2 - 24 March 2012 through 1 April 2012
ER -