Generic Emptiness Check for Fun and Profit

D 2019

Generic Emptiness Check for Fun and Profit

BAIER, Christel, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, David MÜLLER et. al.

Základní údaje

Originální název

Generic Emptiness Check for Fun and Profit

Autoři

BAIER, Christel (276 Německo), František BLAHOUDEK (203 Česká republika), Alexandre DURET-LUTZ (756 Švýcarsko), Joachim KLEIN (276 Německo), David MÜLLER (276 Německo) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Cham (Switzerland), Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, od s. 445-461, 17 s. 2019

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10200 1.2 Computer and information sciences

Stát vydavatele

Švýcarsko

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Kód RIV

RIV/00216224:14330/19:00107786

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-31783-6

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-31784-3_26

UT WoS

000723515700026

Klíčová slova anglicky

TELA; Emerson-Lei automata; emptiness check; probabilistic model checking

Štítky

core_A, firank_A, formal verification, formela-conference, Model checking, 𝜔-automata

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 4. 2020 11:04, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

GA19-24397S, projekt VaV

Název: Automaty v rozhodovacích procedurách a verifikaci (Akronym: AUTODEV)

Investor: Grantová agentura ČR, Automata for Decision Procedures and Verification

Citovat

BAIER, Christel, František BLAHOUDEK, Alexandre DURET-LUTZ, Joachim KLEIN, David MÜLLER a 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, s. 445-461. ISBN 978-3-030-31783-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31784-3_26.

@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 a 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, s.~445-461. ISBN~978-3-030-31783-6. Dostupné z: https://dx.doi.org/10.1007/978-3-030-31784-3\_{}26.

Podrobný výpis o publikaci