Helmut Seidl and Andreas Reuß. Extending H1-Clauses with Path Disequalities. In Lars Birkedal, editor, FoSSaCS, pages 165-179, 2012. Springer, LNCS 7213.

We extend H1-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.

Reference: Bibtex