Local Quantitative LTL Model Checking
Authors | |
---|---|
Year of publication | 2008 |
Type | Article in Proceedings |
Conference | 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008) |
MU Faculty or unit | |
Citation | |
Field | Informatics |
Keywords | LTL Model Checking; Probabilistic; Parallel |
Description | 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. |
Related projects: |