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 Formal Methods for Industrial Critical Systems. Neuveden : Springer Berlin / Heidelberg, 2009. ISBN 978-3-642-03239-4, pp. 53-68. 2008, L'Aquila, Italy. |
| Original language: | English |
| Field: | Informatika |
| WWW: |  http://dx.doi.org/10.1007/978-3-642-03240-0_8 |
| Type: | Article in Proceedings |
| Keywords: | Quantitative Model Checking; Linear Temporal Logic; Probabilistic systems |
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.
Related projects:
- Techniques for automatic verification and validation of software nad hardware systems
- Automated software verification
