enter search term and/or author name
A fast algorithm and datalog inexpressibility for temporal reasoning
Manuel Bodirsky, Jan Kára
Article No.: 15
We introduce a new tractable temporal constraint language, which strictly contains the Ord-Horn language of Bürkert and Nebel and the class of AND/OR precedence constraints. The algorithm we present for this language decides whether a given...
On the completeness of compositional reasoning methods
Kedar S. Namjoshi, Richard J. Trefler
Article No.: 16
Hardware systems and reactive software systems can be described as the composition of several concurrently active processes. Automated reasoning based on model checking algorithms can substantially increase confidence in the overall reliability of...
Deciding strategy properties of contract-signing protocols
Detlef Kähler, Ralf Küsters, Thomas Wilke
Article No.: 17
Research on the automatic analysis of cryptographic protocols has so far concentrated on reachability properties, such as secrecy and authentication. In this article, we prove that certain game-theoretic security properties, including balance for...
Complexity of propositional proofs under a promise
Nachum Dershowitz, Iddo Tzameret
Article No.: 18
We study—within the framework of propositional proof complexity—the problem of certifying unsatisfiability of CNF formulas under the promise that any satisfiable formula has many satisfying assignments, where many stands for an...
Lower bounds for bounded depth Frege proofs via Pudlák-Buss games
Eli Ben-Sasson, Prahladh Harsha
Article No.: 19
We present a simple proof of the bounded-depth Frege proof lower bounds of Pitassi et al.  and Krajíček et al.  for the pigeonhole principle. Our method uses the interpretation of proofs as two player games given by...
In this article, we investigate LTL specifications where γ[ϕ ∧ ψ] is equivalent to γ[ϕ] ∧ γ[ψ] independent of ϕ and ψ. Formulas γ with this property are called distributive queries...