Symbolic Model Checking of Stutter Invariant Properties Using Generalized Testing Automata

Authors

Ala Eddine Ben Salem, Alexandre Duret-Lutz, Fabrice Kordon, Yann Thierry-Mieg

Where

Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14)

Place

Grenoble, France

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2014-04-01

Abstract

In a previous work, we showed that a kind of $\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.

Documents

• Paper

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},
  address	= {Grenoble, France},
  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.}
}