REPORTS > KEYWORD > MODEL CHECKING:
Reports tagged with model checking:
TR01-051
| 4th May 2001
Sophie Laplante, Richard Lassaigne, Frederic Magniez, Sylvain Peyronnet, Michel de Rougemont
Sophie Laplante, Richard Lassaigne, Frederic Magniez, Sylvain Peyronnet, Michel de Rougemont
Probabilistic abstraction for model checking: An approach based on property testing
Revisions: 1
In model checking, program correctness on all inputs is verified by considering the transition system underlying a given program. In practice, the system can be intractably large. In property testing, a property of a single input is verified by looking at a small subset of that input. We join the ...
more >>>
TR08-028
| 5th December 2007
Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer
Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer
The Tractability of Model-Checking for LTL: The Good, the Bad, and the Ugly Fragments
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 set of temporal operators used. If, in contrast, the set of propositional operators is restricted, the complexity may decrease. This paper systematically studies ...
more >>>