Další formáty:
BibTeX
LaTeX
RIS
@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.
|