APMC 3.0: Approximate verification of Discrete and Continuous Time Markov Chains
From LRDE
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
- Authors
- Thomas Hérault, Richard Lassaigne, Sylvain Peyronnet
- Where
- Proceedings of Qest 2006
- Type
- inproceedings
- Projects
- APMC
- Date
- 2006-01-01
Abstract
In this paper, we give a brief overview of APMC (Approximate Probabilistic Model Checker). APMC is a model checker that implements approximate probabilistic verification of probabilistic systems. It is based on Monte-Carlo method and the theory of randomized approximation schemes and allows to verify extremely large models without explicitly representing the global transition system. To avoid the state-space explosion phenomenon, APMC gives an accurate approximation of the satisfaction probability of the property instead of the exact value, but using only a very small amount of memory. The version of APMC we present in this paper can now handle efficiently both discrete and continuous time probabilistic systems.
Bibtex (lrde.bib)
@InProceedings{ herault.06.qest,
author = {Thomas H\'erault and Richard Lassaigne and Sylvain
Peyronnet},
title = {{APMC 3.0}: Approximate verification of Discrete and
Continuous Time Markov Chains},
booktitle = {Proceedings of Qest 2006},
year = 2006,
pages = {129--130},
abstract = {In this paper, we give a brief overview of APMC
(Approximate Probabilistic Model Checker). APMC is a model
checker that implements approximate probabilistic
verification of probabilistic systems. It is based on
Monte-Carlo method and the theory of randomized
approximation schemes and allows to verify extremely large
models without explicitly representing the global
transition system. To avoid the state-space explosion
phenomenon, APMC gives an accurate approximation of the
satisfaction probability of the property instead of the
exact value, but using only a very small amount of memory.
The version of APMC we present in this paper can now handle
efficiently both discrete and continuous time probabilistic
systems.}
}