MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
The result's identifiers
Result code in 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>
Result on the web
<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>
Alternative languages
Result language
angličtina
Original language name
MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
IN - Informatics
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GA15-17564S" target="_blank" >GA15-17564S: Game Theory in Formal Analysis and Verification of Computer Systems</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
Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016
ISBN
9783319465197
ISSN
0302-9743
e-ISSN
—
Number of pages
8
Pages from-to
130-137
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
—