Generic Emptiness Check for Fun and Profit

Abstract

We present a new algorithm for checking the emptiness of $\displaystyle \omega$ -automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although both these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity. In fact, the algorithm provides a unifying view on emptiness checks for these simpler automata classes. We have implemented the algorithm in Spot and PRISM and our experiments show improved performance over previous solutions.

Bibtex (lrde.bib)

@InProceedings{	  baier.19.atva,
author	= {Christel Baier and Franti\v{s}ek Blahoudek and Alexandre
Duret-Lutz and Joachim Klein and David M\"uller and Jan
Strej\v{c}ek},
title		= {Generic Emptiness Check for Fun and Profit},
booktitle	= {Proceedings of the 17th International Symposium on
Automated Technology for Verification and Analysis
(ATVA'19)},
year		= {2019},
volume	= {11781},
series	= {Lecture Notes in Computer Science},
pages		= {445--461},
month		= oct,
publisher	= {Springer},
abstract	= {We present a new algorithm for checking the emptiness of
$\omega$-automata with an Emerson-Lei acceptance condition
(i.e., a positive Boolean formula over sets of states or
transitions that must be visited infinitely or finitely
often). The algorithm can also solve the model checking
problem of probabilistic positiveness of MDP under a
property given as a deterministic Emerson-Lei automaton.
Although both these problems are known to be NP-complete
and our algorithm is exponential in general, it runs in
polynomial time for simpler acceptance conditions like
generalized Rabin, Streett, or parity. In fact, the
algorithm provides a unifying view on emptiness checks for
these simpler automata classes. We have implemented the
algorithm in Spot and PRISM and our experiments show
improved performance over previous solutions.},
doi		= {10.1007/978-3-030-31784-3_26}
}