Publication details
Local Quantitative LTL Model Checking
| Basic information | |
|---|---|
| Original title: | Local Quantitative LTL Model Checking |
| Authors: | Jiří Barnat, Luboš Brim, Ivana Černá, Milan Češka, Jana Tůmová |
| Further information | |
|---|---|
| Citation: | BARNAT, Jiří  - BRIM, Luboš - ČERNÁ, Ivana - ČEŠKA, Milan - TŮMOVÁ, Jana. Local Quantitative LTL Model Checking. In 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2008). L'Aquilla : ERCIM, 2008. ISBN 978-3-642-03239-4, pp. 63-78. 2008, L'Aquilla. |
| Original language: | English |
| Field: | Informatika |
| Type: | Article in Proceedings |
| Keywords: | LTL Model Checking; Probabilistic; Parallel |
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:
- Techniques for automatic verification and validation of software nad hardware systems
- Institute for Theoretical Computer Science
- Automated software verification
