Working Seminar on Formal Models, Discrete Structures, and Algorithms

Stutter-Invariance Checks & Testing Automata

Alexandre Duret-Lutz (EPITA Research and Development Laboratory)

When: April 9, 2pm

Where: room C417


Stutter-Invariant properties are usually used to enable Partial-Order Reductions during model checking. We first describe seven practical checks to decide if an LTL or PSL property is stutter-invariant: they are all based on one or two operators that are simple to implement (joint work with Thibaud Michaud). Then we show how model checking of stutter-invariant properties can be done using different variants of testing-automata: a type of automata that tracks changes to atomic propositions instead of tracking their values (joint work with Ala Eddine Ben Salem and Fabrice Kordon). The connection between these two parts is a normal form (introduced by Etessami) for automata representing stutter-invariant properties.