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

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>

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.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

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)

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ů

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

—