Approximate Model Checking
Probabilistic abstraction .
Given a program and a property to check, which admits some tester, we study how to find, in a general way, some probabilistic abstraction, defined in [LLMPR]. Such an abstraction is a program transformation allowing to abstract certain variables with respect to the tester. We can then apply the test to concrete programs and approximatively check a property in constant time.
Probabilistic Model Checking.
Model Checking has been recently extended to probabilistic protocols, which can be represented by probabilistic transition systems (Markov chains). The objective is to compute the satisfaction probability of some temporal property as reachability, liveness or safety.
The main problem is the space complexity of these methods. A natural issue is to approximate this probability. Although the problem is not approximable in full generality, there exist some randomized approximation schemes in polynomial time for certain classes of properties [LP]. We apply some sampling techniques, as Monte-Carlo method, to probabilistic protocols in order to generate randomized execution paths and approximatively verify these quantitative properties.
Publications
- R. Lassaigne, and S. Peyronnet:
Probabilistic Verification and Approximation, Proceedings WoLLIC 2005, ENTCS 143:101-114, 2006.
- T. Herault, R. Lassaigne, F. Magniette, and S. Peyronnet:
Approximate Probabilistic Model Checking
Proc. of the 5th Conf. on Verification, Model Checking and Abstract Interpretation (VMCAI 2004) Lecture Notes in Computer Science n° 2937, p.73-84.
- M. Duflot, L. Fribourg, T. Herault, R. Lassaigne, F. Magniette,
Stephane Messika, S. Peyronnet and C. Picaronny
Proc. of the 4th Int. Worshop on Automated Verificationof Critical Systems
(AVoCS 2004) Electronic Notes in Theoretical Computer Science 2004.
- S. Laplante, R. Lassaigne, F. Magniez, S. Peyronnet, M. de Rougemont: Probabilistic abstraction for model-checking, LICS 2002, to appear in ACM Transactions on Computational Logic.
- G. Guirado, T. Herault, R. Lassaigne, and S. Peyronnet: Distribution,
Approximation and Probabilistic Model Checking
Proc. Int. Workshop on Parallel and Distributed Methods in Verification, ENTCS 135, 2006.
- T. Herault, R. Lassaigne, and S. Peyronnet: APMC 3.0,
Approximate Verification of Discrete and Continuous time Markov Chains.
Proc. 3rd Int. Conference on Quantitative Evaluation of Systems, 2006.
- M. Cadilhac, T. Herault, R. Lassaigne, and S. Tixeuil:
Evaluating Complex MAC protocols for sensor networks with APMC,
Proc. of the 6th Int. Workshop on Automated Verification of Critical Systems, 2006.