Extending H 1-clauses with path disequalities

Abstract

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. © 2012 Springer-Verlag Berlin Heidelberg.