MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata

Logo poskytovatele

Varování

Publikace nespadá pod Fakultu sportovních studií, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.
Autoři

SICKERT Salomon KŘETÍNSKÝ Jan

Rok publikování 2016
Druh Článek ve sborníku
Konference Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016
Fakulta / Pracoviště MU

Fakulta informatiky

Citace
Doi http://dx.doi.org/10.1007/978-3-319-46520-3_9
Obor Informatika
Klíčová slova probabilistic model checking; verification; automata; temporal logic
Popis 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.
Související projekty:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info