MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
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%3A00088473" target="_blank" >RIV/00216224:14330/16:00088473 - isvavai.cz</a>
Výsledek na webu
<a href="http://dx.doi.org/10.1007/978-3-319-46520-3_9" target="_blank" >http://dx.doi.org/10.1007/978-3-319-46520-3_9</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-319-46520-3_9" target="_blank" >10.1007/978-3-319-46520-3_9</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
Popis výsledku v původním jazyce
The limiting factor for quantitative analysis of Markov decision processes (MDP) against specifications given in linear temporal logic (LTL) is the size of the generated product. As recently shown, a special subclass of limit-deterministic Büchi automata (LDBA) can replace deterministic Rabin automata in quantitative probabilistic model checking algorithms. We present an extension of PRISM for LTL model checking of MDP using LDBA. While existing algorithms can be used only with minimal changes, the new approach takes advantage of the special structure and the smaller size of the obtained LDBA to speed up the model checking. We demonstrate the speed up experimentally by a comparison with other approaches.
Název v anglickém jazyce
MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
Popis výsledku anglicky
The limiting factor for quantitative analysis of Markov decision processes (MDP) against specifications given in linear temporal logic (LTL) is the size of the generated product. As recently shown, a special subclass of limit-deterministic Büchi automata (LDBA) can replace deterministic Rabin automata in quantitative probabilistic model checking algorithms. We present an extension of PRISM for LTL model checking of MDP using LDBA. While existing algorithms can be used only with minimal changes, the new approach takes advantage of the special structure and the smaller size of the obtained LDBA to speed up the model checking. We demonstrate the speed up experimentally by a comparison with other approaches.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
IN - Informatika
OECD FORD obor
—
Návaznosti výsledku
Projekt
<a href="/cs/project/GA15-17564S" target="_blank" >GA15-17564S: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů</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
Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016
ISBN
9783319465197
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
8
Strana od-do
130-137
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
—