In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the s...
Michael Bauland, Martin Mundhenk, Thomas Schneider...
In a seminal paper from 1985, Sistla and Clarke showed that the model-checking problem for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the se...
Michael Bauland, Martin Mundhenk, Thomas Schneider...
The model-checking problem for a logic L on a class C of structures asks whether a given L-sentence holds in a given structure in C. In this paper, we give super-exponential lower...
The compositional method, introduced by Feferman and Vaught in 1959, allows to reduce the model-checking problem for a product structure to the model-checking problem for its fact...
Probabilistic timed automata are an extension of timed automata with discrete probability distributions. We consider model-checking algorithms for the subclasses of probabilistic t...
In this paper we study the complexity of the model-checking problem for the tree logic introduced as the basis for the query language TQL [Cardelli and Ghelli, 2001]. We define tw...