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: 1In 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 ...
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.
...
more >>>