Generic Emptiness Check for Fun and Profit

Publikation: Beitrag in Buch/Konferenzbericht/Sammelband/GutachtenBeitrag in KonferenzbandBeigetragen

Beitragende

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

OriginalspracheEnglisch
TitelAutomated Technology for Verification and Analysis
Redakteure/-innenYu-Fang Chen, Chih-Hong Cheng, Javier Esparza
Herausgeber (Verlag)Springer, Berlin [u. a.]
Seiten445–461
ISBN (Print)978-3-030-31783-6
PublikationsstatusVeröffentlicht - 2019
Peer-Review-StatusNein

Publikationsreihe

ReiheLecture Notes in Computer Science, Volume 11781
ISSN0302-9743

Konferenz

Titel17th International Symposium on Automated Technology for Verification and Analysis
KurztitelATVA 2019
Dauer28 - 31 Oktober 2019
BekanntheitsgradInternationale Veranstaltung
OrtAcademia Sinica
StadtTaipei
LandTaiwan

Externe IDs

ORCID /0000-0002-5321-9343/work/142236712

Schlagworte

Schlagwörter

  • generic emptiness, check, fun, profit

Bibliotheksschlagworte