Other formats:
BibTeX
LaTeX
RIS
@inproceedings{792968,
author = {Barnat, Jiří and Brim, Luboš and Černá, Ivana and Češka, Milan and Tůmová, Jana},
address = {L'Aquilla},
booktitle = {13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008)},
keywords = {LTL Model Checking; Probabilistic; Parallel},
language = {eng},
location = {L'Aquilla},
isbn = {978-3-642-03239-4},
pages = {63-78},
publisher = {ERCIM},
title = {Local Quantitative LTL Model Checking},
year = {2008}
}
TY - JOUR
ID - 792968
AU - Barnat, Jiří - Brim, Luboš - Černá, Ivana - Češka, Milan - Tůmová, Jana
PY - 2008
TI - Local Quantitative LTL Model Checking
PB - ERCIM
CY - L'Aquilla
SN - 9783642032394
KW - LTL Model Checking
KW - Probabilistic
KW - Parallel
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 can be significantly outperformed by a dedicated local model checking one. In this paper we resent 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{13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008)}. L'Aquilla: ERCIM, 2008, p.~63-78. ISBN~978-3-642-03239-4.
|
