SICKERT, Salomon and Jan KŘETÍNSKÝ. MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata. Online. In Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016. Switzerland: Springer, 2016. p. 130-137. ISBN 978-3-319-46519-7. Available from: https://dx.doi.org/10.1007/978-3-319-46520-3_9. [citováno 2024-04-23]
Other formats:   BibTeX LaTeX RIS
Basic information
Original name MoChiBA: Probabilistic {LTL} Model Checking Using Limit-Deterministic Büchi Automata
Authors SICKERT, Salomon (276 Germany) and Jan KŘETÍNSKÝ (203 Czech Republic, guarantor, belonging to the institution)
Edition Switzerland, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, p. 130-137, 8 pp. 2016.
Publisher Springer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher Switzerland
Confidentiality degree is not subject to a state or trade secret
Publication form printed version "print"
Impact factor Impact factor: 0.402 in 2005
RIV identification code RIV/00216224:14330/16:00088473
Organization unit Faculty of Informatics
ISBN 978-3-319-46519-7
ISSN 0302-9743
Doi http://dx.doi.org/10.1007/978-3-319-46520-3_9
UT WoS 000389808100009
Keywords in English probabilistic model checking; verification; automata; temporal logic
Tags core_A, firank_A, formela-conference
Tags International impact, Reviewed
Changed by Changed by: RNDr. Pavel Šmerk, Ph.D., učo 3880. Changed: 1/6/2022 12:40.
Abstract
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.
Links
GA15-17564S, research and development projectName: Teorie her jako prostředek pro formální analýzu a verifikaci počítačových systémů
Investor: Czech Science Foundation
PrintDisplayed: 23/4/2024 12:25