Generic Emptiness Check for Fun and Profit

Investor logo

Warning

This publication doesn't include Faculty of Arts. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

BAIER Christel BLAHOUDEK František DURET-LUTZ Alexandre KLEIN Joachim MÜLLER David STREJČEK Jan

Year of publication 2019
Type Article in Proceedings
Conference Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings
MU Faculty or unit

Faculty of Informatics

Citation
Web https://link.springer.com/chapter/10.1007/978-3-030-31784-3_26
Doi http://dx.doi.org/10.1007/978-3-030-31784-3_26
Keywords TELA; Emerson-Lei automata; emptiness check; probabilistic model checking
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.