Three SCC-based Emptiness Checks for Generalized Büchi Automata

Authors

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

Where

Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'13)

Type

inproceedings

Publisher

Springer

Date

2013-10-09

Abstract

The automata-theoretic approach for the verification of linear time properties involves checking the emptiness of a Büchi automaton. However generalized Büchi automata, with multiple acceptance sets, are preferred when verifying under weak fairness hypotheses. Existing emptiness checks for which the complexity is independent of the number of acceptance sets are all based on the enumeration of Strongly Connected Components (SCCs). In this paper, we review the state of the art SCC enumeration algorithms to study how they can be turned into emptiness checks. This leads us to define two new emptiness check algorithms (one of them based on the Union Find data structure), introduce new optimizations, and show that one of these can be of benefit to a classic SCCs enumeration algorithm. We have implemented all these variants to compare their relative performances and the overhead induced by the emptiness check compared to the corresponding SCCs enumeration algorithm. Our experiments shows that these three algorithms are comparable.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  renault.13.lpar,
  author	= {Etienne Renault and Alexandre Duret-Lutz and Fabrice
		  Kordon and Denis Poitrenaud},
  title		= {Three {SCC}-based Emptiness Checks for Generalized
		  {B\"u}chi Automata},
  booktitle	= {Proceedings of the 19th International Conference on Logic
		  for Programming, Artificial Intelligence, and Reasoning
		  (LPAR'13)},
  editor	= {Ken McMillan and Aart Middeldorp and Andrei Voronkov },
  year		= 2013,
  month		= dec,
  pages		= {668--682},
  publisher	= {Springer},
  series	= {Lecture Notes in Computer Science},
  volume	= 8312,
  abstract	= {The automata-theoretic approach for the verification of
		  linear time properties involves checking the emptiness of a
		  B{\"u}chi automaton. However generalized B{\"u}chi
		  automata, with multiple acceptance sets, are preferred when
		  verifying under weak fairness hypotheses. Existing
		  emptiness checks for which the complexity is independent of
		  the number of acceptance sets are all based on the
		  enumeration of Strongly Connected Components (SCCs). In
		  this paper, we review the state of the art SCC enumeration
		  algorithms to study how they can be turned into emptiness
		  checks. This leads us to define two new emptiness check
		  algorithms (one of them based on the Union Find data
		  structure), introduce new optimizations, and show that one
		  of these can be of benefit to a classic SCCs enumeration
		  algorithm. We have implemented all these variants to
		  compare their relative performances and the overhead
		  induced by the emptiness check compared to the
		  corresponding SCCs enumeration algorithm. Our experiments
		  shows that these three algorithms are comparable.},
  doi		= {10.1007/978-3-642-45221-5_44}
}