Generic Emptiness Check for Fun and Profit

Christel BaierChristel Baier, František BlahoudekFrantišek Blahoudek, Alexandre Duret-LutzAlexandre Duret-Lutz, Joachim KleinJoachim Klein, David MüllerDavid Müller, Jan StrejčekJan Strejček

DOI Link

Christel Baier, František Blahoudek, Alexandre Duret-Lutz, Joachim Klein, David Müller, Jan Strejček
Generic Emptiness Check for Fun and Profit
Proc. of 17th International Symposium on Automated Technology for Verification and Analysis, volume 11781 of Lecture Notes in Computer Science, 445-461, 2019. Springer

Details
Bibtex

KurzfassungAbstract
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.
Forschungsgruppe:Research Group: Algebraische und logische Grundlagen der InformatikAlgebraic and Logical Foundations of Computer Science

The final publication is available at Springer via http://dx.doi.org/10.1007/978-3-030-31784-3_26.

@inproceedings{BBDKMS2019,
  author    = {Christel Baier and Franti{\v{s}}ek Blahoudek and Alexandre
               Duret-Lutz and Joachim Klein and David M{\"{u}}ller and Jan
               Strej{\v{c}}ek},
  title     = {Generic Emptiness Check for Fun and Profit},
  booktitle = {Proc. of 17th International Symposium on Automated Technology for
               Verification and Analysis},
  series    = {Lecture Notes in Computer Science},
  volume    = {11781},
  publisher = {Springer},
  year      = {2019},
  pages     = {445-461},
  doi       = {10.1007/978-3-030-31784-3_26}
}