Další formáty:
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 a 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, s.~63-78. ISBN~978-3-642-03239-4.
|