Combining Explicit and Symbolic Approaches for Better On-the-Fly LTL Model Checking

Authors

Alexandre Duret-Lutz, Kais Klai, Denis Poitrenaud, Yann Thierry-Mieg

Type

techreport

Date

2011-06-01

Abstract

We present two new hybrid techniques that replace the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed products are explicit graphs of aggregates (symbolic sets of states) that can be interpreted as Büchi automata. These hybrid approaches allow on the one hand to use classical emptiness-check algorithms and build the graph on-the-flyand on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates. The Symbolic Observation Product assumes a globally stuttering property (e.g., LTL-X) to aggregate states. The Self-Loop Aggregation Product does not require the property to be globally stuttering (i.e., it can tackle full LTL), but dynamically detects and exploits a form of stuttering where possible. Our experiments show that these two variants, while incomparable with each other, can outperform other existing approaches.

Bibtex (lrde.bib)

@TechReport{	  duret.11.arxiv,
  author	= {Alexandre Duret-Lutz and Kais Klai and Denis Poitrenaud
		  and Yann Thierry-Mieg},
  title		= {Combining Explicit and Symbolic Approaches for Better
		  On-the-Fly {LTL} Model Checking},
  institution	= {arXiv},
  year		= 2011,
  number	= {1106.5700},
  month		= jun,
  note		= {Extended version of our ATVA'11 paper, presenting two new
		  techniques instead of one.},
  url		= {http://arxiv.org/abs/1106.5700},
  abstract	= {We present two new hybrid techniques that replace the
		  synchronized product used in the automata-theoretic
		  approach for LTL model checking. The proposed products are
		  explicit graphs of aggregates (symbolic sets of states)
		  that can be interpreted as B\"uchi automata. These hybrid
		  approaches allow on the one hand to use classical
		  emptiness-check algorithms and build the graph on-the-fly,
		  and on the other hand, to have a compact encoding of the
		  state space thanks to the symbolic representation of the
		  aggregates. The \emph{Symbolic Observation Product} assumes
		  a globally stuttering property (e.g., LTL-X) to aggregate
		  states. The \emph{Self-Loop Aggregation Product} does not
		  require the property to be globally stuttering (i.e., it
		  can tackle full LTL), but dynamically detects and exploits
		  a form of stuttering where possible. Our experiments show
		  that these two variants, while incomparable with each
		  other, can outperform other existing approaches.}
}