Limit-Deterministic Büchi Automata for Linear Temporal Logic
Identifikátory výsledku
Kód výsledku v 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>
Výsledek na webu
<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>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Limit-Deterministic Büchi Automata for Linear Temporal Logic
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Limit-Deterministic Büchi Automata for Linear Temporal Logic
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GBP202%2F12%2FG061" target="_blank" >GBP202/12/G061: Centrum excelence - Institut teoretické informatiky (CE-ITI)</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2016
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Computer Aided Verification - 28th International Conference, CAV 2016
ISBN
9783319415390
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
21
Strana od-do
312-332
Název nakladatele
Springer
Místo vydání
Switzerland
Místo konání akce
Switzerland
Datum konání akce
1. 1. 2016
Typ akce podle státní příslušnosti
CST - Celostátní akce
Kód UT WoS článku
—