Generic Emptiness Check for Fun and Profit
Research output: Contribution to book/Conference proceedings/Anthology/Report › Conference contribution › Contributed
Contributors
Abstract
We present a new algorithm for checking the emptiness of ω-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.
Details
Original language | English |
---|---|
Title of host publication | Automated Technology for Verification and Analysis |
Editors | Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza |
Publisher | Springer, Berlin [u. a.] |
Pages | 445–461 |
ISBN (print) | 978-3-030-31783-6 |
Publication status | Published - 2019 |
Peer-reviewed | No |
Publication series
Series | Lecture Notes in Computer Science, Volume 11781 |
---|---|
ISSN | 0302-9743 |
Conference
Title | 17th International Symposium on Automated Technology for Verification and Analysis |
---|---|
Abbreviated title | ATVA 2019 |
Duration | 28 - 31 October 2019 |
Degree of recognition | International event |
Location | Academia Sinica |
City | Taipei |
Country | Taiwan, Province of China |
External IDs
ORCID | /0000-0002-5321-9343/work/142236712 |
---|---|
Scopus | 85076098432 |
Keywords
Keywords
- generic emptiness, check, fun, profit