Limit-Deterministic Büchi Automata for Linear Temporal Logic

D 2016

Limit-Deterministic Büchi Automata for Linear Temporal Logic

SICKERT, Salomon, Javier ESPARZA, Stefan JAAX and Jan KŘETÍNSKÝ

Basic information

Original name

Limit-Deterministic Büchi Automata for Linear Temporal Logic

Authors

SICKERT, Salomon (276 Germany), Javier ESPARZA (724 Spain), Stefan JAAX (276 Germany) and Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution)

Edition

Switzerland, Computer Aided Verification - 28th International Conference, CAV 2016, p. 312-332, 21 pp. 2016

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

Confidentiality degree

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

Publication form

printed version "print"

Impact factor

Impact factor: 0.402 in 2005

RIV identification code

RIV/00216224:14330/16:00088472

Organization unit

Faculty of Informatics

ISBN

978-3-319-41539-0

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-41540-6_17

UT WoS

000387731400017

Keywords in English

verification; probabilistic model checking; temporal logic; automata; determinism

Abstract

V originále

Limit-deterministic Büchi automata can replace deterministic Rabin automata in probabilistic model checking algorithms, and can be significantly smaller. We present a direct construction from an LTL formula \phi to a limit-deterministic Büchi automaton. The automaton is the combination of a non-deterministic component, guessing the set of eventually true G-subformulas of \phi , and a deterministic component verifying this guess and using this information to decide on acceptance. Contrary to the indirect approach of constructing a non-deterministic automaton for \phi and then applying a semi-determinisation algorithm, our translation is compositional and has a clear logical structure. Moreover, due to its special structure, the resulting automaton can be used not only for qualitative, but also for quantitative verification of MDPs, using the same model checking algorithm as for deterministic automata. This allows one to reuse existing efficient implementations of this algorithm without any modification. Our construction yields much smaller automata for formulas with deep nesting of modal operators and performs at least as well as the existing approaches on general formulas.

Links

GBP202/12/G061, research and development project

Name: Centrum excelence - Institut teoretické informatiky (CE-ITI) (Acronym: CE-ITI)

Investor: Czech Science Foundation

Citovat

SICKERT, Salomon, Javier ESPARZA, Stefan JAAX and Jan KŘETÍNSKÝ. Limit-Deterministic Büchi Automata for Linear Temporal Logic. In Computer Aided Verification - 28th International Conference, CAV 2016. Switzerland: Springer, 2016, p. 312-332. ISBN 978-3-319-41539-0. Available from: https://dx.doi.org/10.1007/978-3-319-41540-6_17.

@inproceedings{1365651,
   author = {Sickert, Salomon and Esparza, Javier and Jaax, Stefan and Křetínský, Jan},
   address = {Switzerland},
   booktitle = {Computer Aided Verification - 28th International Conference, CAV 2016},
   doi = {http://dx.doi.org/10.1007/978-3-319-41540-6_17},
   keywords = {verification; probabilistic model checking; temporal logic; automata; determinism},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Switzerland},
   isbn = {978-3-319-41539-0},
   pages = {312-332},
   publisher = {Springer},
   title = {Limit-Deterministic Büchi Automata for Linear Temporal Logic},
   year = {2016}
}

TY  - JOUR
ID  - 1365651
AU  - Sickert, Salomon - Esparza, Javier - Jaax, Stefan - Křetínský, Jan
PY  - 2016
TI  - Limit-Deterministic Büchi Automata for Linear Temporal Logic
PB  - Springer
CY  - Switzerland
SN  - 9783319415390
KW  - verification
KW  - probabilistic model checking
KW  - temporal logic
KW  - automata
KW  - determinism
N2  - Limit-deterministic Büchi automata can replace deterministic Rabin automata in probabilistic model checking algorithms, and can be significantly smaller. We present a direct construction from an LTL formula \phi to a limit-deterministic Büchi automaton. The automaton is the combination of a non-deterministic component, guessing the set of eventually true G-subformulas of \phi , and a deterministic component verifying this guess and using this information to decide on acceptance. Contrary to the indirect approach of constructing a non-deterministic automaton for \phi and then applying a semi-determinisation algorithm, our translation is compositional and has a clear logical structure. Moreover, due to its special structure, the resulting automaton can be used not only for qualitative, but also for quantitative verification of MDPs, using the same model checking algorithm as for deterministic automata. This allows one to reuse existing efficient implementations of this algorithm without any modification. Our construction yields much smaller automata for formulas with deep nesting of modal operators and performs at least as well as the existing approaches on general formulas.
ER  -

SICKERT, Salomon, Javier ESPARZA, Stefan JAAX and Jan KŘETÍNSKÝ. Limit-Deterministic Büchi Automata for Linear Temporal Logic. In \textit{Computer Aided Verification - 28th International Conference, CAV 2016}. Switzerland: Springer, 2016, p.~312-332. ISBN~978-3-319-41539-0. Available from: https://dx.doi.org/10.1007/978-3-319-41540-6\_{}17.

Detailed Information on Publication Record