Other formats:
BibTeX
LaTeX
RIS
@inproceedings{856368,
author = {Barnat, Jiří and Brim, Luboš and Černá, Ivana and Češka, Milan and Tůmová, Jana},
address = {Neuveden},
booktitle = {Formal Methods for Industrial Critical Systems},
doi = {http://dx.doi.org/10.1007/978-3-642-03240-0_8},
keywords = {Quantitative Model Checking; Linear Temporal Logic; Probabilistic systems},
howpublished = {tištěná verze "print"},
language = {eng},
location = {Neuveden},
isbn = {978-3-642-03239-4},
pages = {53-68},
publisher = {Springer Berlin / Heidelberg},
title = {Local Quantitative LTL Model Checking},
url = {http://dx.doi.org/10.1007/978-3-642-03240-0_8},
year = {2009}
}
TY - JOUR
ID - 856368
AU - Barnat, Jiří - Brim, Luboš - Černá, Ivana - Češka, Milan - Tůmová, Jana
PY - 2009
TI - Local Quantitative LTL Model Checking
PB - Springer Berlin / Heidelberg
CY - Neuveden
SN - 9783642032394
KW - Quantitative Model Checking
KW - Linear Temporal Logic
KW - Probabilistic systems
UR - http://dx.doi.org/10.1007/978-3-642-03240-0_8
N2 - Quantitative analysis of probabilistic systems has been studied mainly from the global model checking point, of view. In the global model-checking, the goal of verification is to decide the probability of satisfaction of a given property for all reachable states in the state space of the system under investigation. On the other hand, in local model checking approach the probability of satisfaction is computed only for the set of initial states. In theory, it is possible to solve the local model checking problem using the global model checking approach. However, the global model checking procedure call be significantly outperformed by a dedicated local model checking one. In this paper we present several particular local model checking techniques that, if applied to global model checking procedure reduce the runtime needed from days to minutes.
ER -
BARNAT, Jiří, Luboš BRIM, Ivana ČERNÁ, Milan ČEŠKA and Jana TŮMOVÁ. Local Quantitative LTL Model Checking. In \textit{Formal Methods for Industrial Critical Systems}. Neuveden: Springer Berlin / Heidelberg, 2009, p.~53-68. ISBN~978-3-642-03239-4. Available from: https://dx.doi.org/10.1007/978-3-642-03240-0\_{}8.
|
