Sophie Laplante, Richard Lassaigne, Frederic Magniez, Sylvain Peyronnet, Michel de Rougemont

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 ...
more >>>

Michael Bauland, Martin Mundhenk, Thomas Schneider, Henning Schnoor, Ilka Schnoor, Heribert Vollmer

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 >>>

Jiawei Gao, Russell Impagliazzo

Fine-grained reductions, introduced by Vassilevska-Williams and Williams, preserve any improvement in the known algorithms. These have been used very successfully in relating the exact complexities of a wide range of problems, from NP-complete problems like SAT to important quadratic time solvable problems within P such as Edit Distance. However, until ... more >>>