Other formats:
BibTeX
LaTeX
RIS
@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.
|