Publications/bensalem.14.tacas

Authors

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

Where

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

Place

Grenoble, France

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2014-01-01

Abstract

In a previous work, we showed that a kind of ω-automata known as Tran­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 ̈uchi 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	= {{20th International Conference on Tools and Algorithms for
		  the Construction and Analysis of Systems (TACAS)}},
  year		= 2014,
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  optvolume	= {?},
  pages		= {to be published},
  address	= {Grenoble, France},
  month		= {April},
  note		= {Accepted},
  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ü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\ ̈uchi Automata.}
}