Difference between revisions of "Publications/herault.06.qest"
From LRDE
Line 5: | Line 5: | ||
| title = APMC 3.0: Approximate verification of Discrete and Continuous Time Markov Chains |
| title = APMC 3.0: Approximate verification of Discrete and Continuous Time Markov Chains |
||
| booktitle = Proceedings of Qest 2006 |
| booktitle = Proceedings of Qest 2006 |
||
− | | pages = |
+ | | pages = 129 to 130 |
| lrdeprojects = APMC |
| lrdeprojects = APMC |
||
| 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. |
| 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. |
Latest revision as of 18:57, 4 January 2018
- 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.} }