We are please at the following paper has been accepted in the 20th
International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS). Please find the title and abstract
below.
Title and corresponding authors:
Symbolic Model Checking of stutter invariant properties Using
Generalized Testing Automata.
A. Ben Salem(1), A. Duret-Lutz(1), F. Kordon(2), and Y. Thierry-Mieg(2)
(1) LRDE-EPITA,
www.lrde.epita.fr
(2) UPMC-LIP6,
www.lip6.fr
Abstract:
Previous work showed that a kind of omega-automata known as
Transition-based Generalized Testing Automata (TGTA) can outperfrom the
Büchi automata traditionally used for \textit{explicit} model checking
when verifying stutter-invariant properties.
In this work, we investigate the use of these generalized testing
automata to improve \textit{symbolic} model checking of
stutter-invariant LTL properties. We propose an efficient symbolic
encoding of stuttering transitions in the product between a model and a
TGTA. Saturation techniques available for decision diagrams then benefit
from the presence of stuttering self-loops on all states of TGTA.
Experimentation of this approach confirms that it outperforms the
symbolic approach based on (transition-based) Generalized Büchi
Automata.