Publications/renault.13.tacas

Authors

Etienne Renault, Alexandre Duret-Lutz, Fabrice Kordon, Denis Poitrenaud

Where

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

Type

inproceedings

Publisher

Springer

Projects

Spot

Date

2013-01-08

Abstract

The automata-theoretic approach for model checking of linear-time temporal properties involves the emptiness check of a large Büchi automaton. Specialized emptiness-check algorithms have been proposed for the cases where the property is represented by a weak or terminal automaton. When the property automaton does not fall into these categories, a general emptiness check is required. This paper focuses on this class of properties. We refine previous approaches by classifying strongly-connected components rather than automata, and suggest a decomposition of the property automaton into three smaller automata capturing the terminal, weak, and the remaining strong behaviors of the property. The three corresponding emptiness checks can be performed independently, using the most appropriate algorithm. Such a decomposition approach can be used with any automata-based model checker. We illustrate the interest of this new approach using explicit and symbolic LTL model checkers.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  renault.13.tacas,
  author	= {Etienne Renault and Alexandre Duret-Lutz and Fabrice
		  Kordon and Denis Poitrenaud},
  title		= {Strength-Based Decomposition of the Property {B\"u}chi
		  Automaton for Faster Model Checking},
  booktitle	= {Proceedings of the 19th International Conference on Tools
		  and Algorithms for the Construction and Analysis of Systems
		  (TACAS'13)},
  editor	= {Nir Piterman and Scott A. Smolka},
  year		= 2013,
  month		= mar,
  pages		= {580--593},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  volume	= 7795,
  abstract	= {The automata-theoretic approach for model checking of
		  linear-time temporal properties involves the emptiness
		  check of a large B{\"u}chi automaton. Specialized
		  emptiness-check algorithms have been proposed for the cases
		  where the property is represented by a weak or terminal
		  automaton. When the property automaton does not fall into
		  these categories, a general emptiness check is required.
		  This paper focuses on this class of properties. We refine
		  previous approaches by classifying strongly-connected
		  components rather than automata, and suggest a
		  decomposition of the property automaton into three smaller
		  automata capturing the terminal, weak, and the remaining
		  strong behaviors of the property. The three corresponding
		  emptiness checks can be performed independently, using the
		  most appropriate algorithm. Such a decomposition approach
		  can be used with any automata-based model checker. We
		  illustrate the interest of this new approach using explicit
		  and symbolic LTL model checkers.}
}