Single-pass Testing Automata for LTL Model Checking

Authors

Ala Eddine Ben Salem

Where

Proceedings of the 9th International Conference on Language and Automata Theory and Applications (LATA'15)

Place

Nice, France

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2015-03-01

Abstract

Testing Automaton (TA) is a new kind of $\omega$-automaton introduced by Hansen et al. as an alternative to the standard Büchi Automata (BA) for the verification of stutter-invariant LTL properties. Geldenhuys and Hansen shown later how to use TA in the automata-theoretic approach to LTL model checking. They propose a TA-based approach using a verification algorithm that requires two searches (two passes) and compare its performance against the BA approach. This paper improves their work by proposing a transformation of TA into a normal form (STA) that only requires a single one-pass verification algorithm. The resulting automaton is called Single-pass Testing Automaton (STA). We have implemented the STA approach in Spot model checking library. We are thus able to compare it with the "traditional" BA and TA approaches. These experiments show that STA compete well on our examples.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  bensalem.15.lata,
  author	= {Ala Eddine Ben{ S}alem},
  title		= {Single-pass Testing Automata for {LTL} Model Checking},
  booktitle	= {Proceedings of the 9th International Conference on
		  Language and Automata Theory and Applications (LATA'15)},
  year		= 2015,
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  address	= {Nice, France},
  month		= mar,
  volume	= 8977,
  pages		= {563--576},
  abstract	= {Testing Automaton (TA) is a new kind of $\omega$-automaton
		  introduced by Hansen et al. as an alternative to the
		  standard B\"uchi Automata (BA) for the verification of
		  stutter-invariant LTL properties. Geldenhuys and Hansen
		  shown later how to use TA in the automata-theoretic
		  approach to LTL model checking. They propose a TA-based
		  approach using a verification algorithm that requires two
		  searches (two passes) and compare its performance against
		  the BA approach. This paper improves their work by
		  proposing a transformation of TA into a normal form (STA)
		  that only requires a single one-pass verification
		  algorithm. The resulting automaton is called Single-pass
		  Testing Automaton (STA). We have implemented the STA
		  approach in Spot model checking library. We are thus able
		  to compare it with the "traditional" BA and TA approaches.
		  These experiments show that STA compete well on our
		  examples.}
}