# Symbolic Model Checking of Stutter Invariant Properties Using Generalized Testing Automata

### From LRDE

(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)

## Abstract

In a previous work, we showed that a kind of ${\displaystyle \omega }$-automata known as emphTran­sition-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.

## Bibtex (lrde.bib)

@InProceedings{	  bensalem.14.tacas,
author	= {Ala Eddine Ben{ S}alem and Alexandre Duret-Lutz and
Fabrice Kordon and Yann Thierry-Mieg},
title		= {Symbolic Model Checking of Stutter Invariant Properties
Using Generalized Testing Automata},
booktitle	= {Proceedings of the 20th International Conference on Tools
and Algorithms for the Construction and Analysis of Systems
(TACAS'14)},
year		= 2014,
publisher	= {Springer},
doi		= {10.1007/978-3-642-54862-8_38},
series	= {Lecture Notes in Computer Science},
volume	= 8413,
pages		= {440--454},
month		= apr,
abstract	= {In a previous work, we showed that a kind of
$\omega$-automata known as \emph{Tran\-sition-based
Generalized Testing Automata} (TGTA) can outperform the
B\"uchi 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\"uchi Automata.}
}