Extending Testing Automata to All LTL

From LRDE

Abstract

An alternative to the traditional Büchi Automata (BA)called Testing Automata (TA) was proposed by Hansen et al. to improve the automata theoretic approach to LTL model checking. In previous work, we proposed an improvement of this alternative approach called TGTA (Generalized Testing Automata). TGTA mixes features from both TA and TGBA (Generalized Büchi Automata), without the disadvantage of TA, which is the second pass of the emptiness check algorithm. We have shown that TGTA outperform TA, BA and TGBA for explicit and symbolic LTL model checking. HoweverTA and TGTA are less expressive than Büchi Automata since they are able to represent only stutter-invariant LTL properties (LTLX). In this paper, we show how to extend Generalized Testing Automata (TGTA) to represent any LTL property. This allows to extend the model checking approach based on this new form of testing automata to check other kinds of properties and also other kinds of models (such as Timed models). Implementation and experimentation of this extended TGTA approach show that it is statistically more efficient than the Büchi Automata approaches (BA and TGBA), for the explicit model checking of LTL properties.

Documents

Bibtex (lrde.bib)

@InProceedings{	  bensalem.15.forte,
  author	= {Ala Eddine Ben{ S}alem},
  title		= {Extending Testing Automata to All {LTL}},
  booktitle	= {Proceedings of the 35th IFIP International Conference on
		  Formal Techniques for Distributed Objects, Components and
		  Systems (FORTE'15)},
  year		= 2015,
  address	= {Grenoble, France},
  month		= jun,
  series	= {Lecture Notes in Computer Science},
  volume	= 9039,
  publisher	= {Springer},
  abstract	= {An alternative to the traditional {B\"u}chi Automata (BA),
		  called Testing Automata (TA) was proposed by Hansen et al.
		  to improve the automata theoretic approach to LTL model
		  checking. In previous work, we proposed an improvement of
		  this alternative approach called TGTA (Generalized Testing
		  Automata). TGTA mixes features from both TA and TGBA
		  (Generalized {B\"u}chi Automata), without the disadvantage
		  of TA, which is the second pass of the emptiness check
		  algorithm. We have shown that TGTA outperform TA, BA and
		  TGBA for explicit and symbolic LTL model checking. However,
		  TA and TGTA are less expressive than {B\"u}chi Automata
		  since they are able to represent only stutter-invariant LTL
		  properties (LTL\X). In this paper, we show how to extend
		  Generalized Testing Automata (TGTA) to represent any LTL
		  property. This allows to extend the model checking approach
		  based on this new form of testing automata to check other
		  kinds of properties and also other kinds of models (such as
		  Timed models). Implementation and experimentation of this
		  extended TGTA approach show that it is statistically more
		  efficient than the {B\"u}chi Automata approaches (BA and
		  TGBA), for the explicit model checking of LTL properties. }
}