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

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

Nakladatel

Springer

Další údaje

Jazyk

angličtina

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

ISBN

978-3-319-46519-7

ISSN

DOI

http://dx.doi.org/10.1007/978-3-319-46520-3_9

UT WoS

000389808100009

Klíčová slova anglicky

probabilistic model checking; verification; automata; temporal logic

Štítky

core_A, firank_A, formela-conference

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 1. 6. 2022 12:40, RNDr. Pavel Šmerk, Ph.D.

Anotace

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ů

Citovat

SICKERT, Salomon a Jan KŘETÍNSKÝ. MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata. In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Switzerland: Springer, 2016, s. 130-137. ISBN 978-3-319-46519-7. Dostupné z: https://dx.doi.org/10.1007/978-3-319-46520-3_9.

@inproceedings{1365656,
   author = {Sickert, Salomon and Křetínský, Jan},
   address = {Switzerland},
   booktitle = {Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016},
   doi = {http://dx.doi.org/10.1007/978-3-319-46520-3_9},
   keywords = {probabilistic model checking; verification; automata; temporal logic},
   howpublished = {tištěná verze "print"},
   language = {eng},
   location = {Switzerland},
   isbn = {978-3-319-46519-7},
   pages = {130-137},
   publisher = {Springer},
   title = {MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata},
   year = {2016}
}

TY  - JOUR
ID  - 1365656
AU  - Sickert, Salomon - Křetínský, Jan
PY  - 2016
TI  - MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
PB  - Springer
CY  - Switzerland
SN  - 9783319465197
KW  - probabilistic model checking
KW  - verification
KW  - automata
KW  - temporal logic
N2  - 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.
ER  -

SICKERT, Salomon a Jan KŘETÍNSKÝ. MoChiBA: Probabilistic $\{$LTL$\}$ Model Checking Using Limit-Deterministic Büchi Automata. In \textit{Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016}. Switzerland: Springer, 2016, s.~130-137. ISBN~978-3-319-46519-7. Dostupné z: https://dx.doi.org/10.1007/978-3-319-46520-3\_{}9.

Podrobný výpis o publikaci