Limit-Deterministic Büchi Automata for Linear Temporal Logic
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F16%3A00088472" target="_blank" >RIV/00216224:14330/16:00088472 - isvavai.cz</a>
Result on the web
<a href="http://dx.doi.org/10.1007/978-3-319-41540-6_17" target="_blank" >http://dx.doi.org/10.1007/978-3-319-41540-6_17</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-41540-6_17" target="_blank" >10.1007/978-3-319-41540-6_17</a>
Alternative languages
Result language
angličtina
Original language name
Limit-Deterministic Büchi Automata for Linear Temporal Logic
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Center of excellence - Institute for theoretical computer science (CE-ITI)</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2016
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Computer Aided Verification - 28th International Conference, CAV 2016
ISBN
9783319415390
ISSN
0302-9743
e-ISSN
—
Number of pages
21
Pages from-to
312-332
Publisher name
Springer
Place of publication
Switzerland
Event location
Switzerland
Event date
Jan 1, 2016
Type of event by nationality
CST - Celostátní akce
UT code for WoS article
—