D
2016
MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
SICKERT, Salomon a Jan KŘETÍNSKÝ
Základní údaje
Originální název
MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
Autoři
SICKERT, Salomon (276 Německo) a
Jan KŘETÍNSKÝ (203 Česká republika, garant, domácí)
Vydání
Switzerland, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, od s. 130-137, 8 s. 2016
Další údaje
Typ výsledku
Stať ve sborníku
Obor
10201 Computer sciences, information science, bioinformatics
Stát vydavatele
Švýcarsko
Utajení
není předmětem státního či obchodního tajemství
Forma vydání
tištěná verze "print"
Impakt faktor
Impact factor: 0.402 v roce 2005
Kód RIV
RIV/00216224:14330/16:00088473
Organizační jednotka
Fakulta informatiky
Klíčová slova anglicky
probabilistic model checking; verification; automata; temporal logic
Příznaky
Mezinárodní význam, Recenzováno
V originále
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ávaznosti
GA15-17564S, projekt VaV | Název: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů | Investor: Grantová agentura ČR, Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů |
|
Zobrazeno: 7. 11. 2024 22:47