BAIER, Christel, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, David MÜLLER and Jan STREJČEK. Generic Emptiness Check for Fun and Profit. Online. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings. Cham (Switzerland): Springer, 2019, p. 445-461. ISBN 978-3-030-31783-6. Available from: https://dx.doi.org/10.1007/978-3-030-31784-3_26. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{1579475, author = {Baier, Christel and Blahoudek, František and DuretandLutz, Alexandre and Klein, Joachim and Müller, David and Strejček, Jan}, address = {Cham (Switzerland)}, booktitle = {Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings}, doi = {http://dx.doi.org/10.1007/978-3-030-31784-3_26}, editor = {Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza}, keywords = {TELA; Emerson-Lei automata; emptiness check; probabilistic model checking}, howpublished = {elektronická verze "online"}, language = {eng}, location = {Cham (Switzerland)}, isbn = {978-3-030-31783-6}, pages = {445-461}, publisher = {Springer}, title = {Generic Emptiness Check for Fun and Profit}, url = {https://link.springer.com/chapter/10.1007/978-3-030-31784-3_26}, year = {2019} }
TY - JOUR ID - 1579475 AU - Baier, Christel - Blahoudek, František - Duret-Lutz, Alexandre - Klein, Joachim - Müller, David - Strejček, Jan PY - 2019 TI - Generic Emptiness Check for Fun and Profit PB - Springer CY - Cham (Switzerland) SN - 9783030317836 KW - TELA KW - Emerson-Lei automata KW - emptiness check KW - probabilistic model checking UR - https://link.springer.com/chapter/10.1007/978-3-030-31784-3_26 L2 - https://link.springer.com/chapter/10.1007/978-3-030-31784-3_26 N2 - 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. ER -
BAIER, Christel, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, David MÜLLER and Jan STREJČEK. Generic Emptiness Check for Fun and Profit. Online. In Yu-Fang Chen, Chih-Hong Cheng, Javier Esparza. \textit{Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings}. Cham (Switzerland): Springer, 2019, p.~445-461. ISBN~978-3-030-31783-6. Available from: https://dx.doi.org/10.1007/978-3-030-31784-3\_{}26.
|