In a previous work, we showed that a kind of ω-automata known as Transition-based Generalized Testing Automata (TGTA) can outperform the Büchi automata traditionally used for explicit model checking when verifying stutter-invariant properties. In this work, we investigate the use of these generalized testing automata to improve 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. © 2014 Springer-Verlag.
CITATION STYLE
Ben Salem, A. E., Duret-Lutz, A., Kordon, F., & Thierry-Mieg, Y. (2014). Symbolic model checking of stutter-invariant properties using generalized testing automata. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8413 LNCS, pp. 440–454). Springer Verlag. https://doi.org/10.1007/978-3-642-54862-8_38
Mendeley helps you to discover research relevant for your work.