Difference between revisions of "Publications/herault.06.qest"
From LRDE
| (3 intermediate revisions by the same user not shown) | |||
| Line 1: | Line 1: | ||
{{Publication |
{{Publication |
||
| + | | published = true |
||
| date = 2006-01-01 |
| date = 2006-01-01 |
||
| authors = Thomas Hérault, Richard Lassaigne, Sylvain Peyronnet |
| authors = Thomas Hérault, Richard Lassaigne, Sylvain Peyronnet |
||
| Line 5: | Line 6: | ||
| booktitle = Proceedings of Qest 2006 |
| booktitle = Proceedings of Qest 2006 |
||
| pages = 129 to 130 |
| pages = 129 to 130 |
||
| − | | project = APMC |
||
| − | | urllrde = 200606-Qest |
||
| ⚫ | | 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. |
||
| 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. |
||
| type = inproceedings |
| type = inproceedings |
||
| id = herault.06.qest |
| id = herault.06.qest |
||
| Line 20: | Line 19: | ||
year = 2006, |
year = 2006, |
||
pages = <nowiki>{</nowiki>129--130<nowiki>}</nowiki>, |
pages = <nowiki>{</nowiki>129--130<nowiki>}</nowiki>, |
||
| − | project = <nowiki>{</nowiki>APMC<nowiki>}</nowiki>, |
||
abstract = <nowiki>{</nowiki>In this paper, we give a brief overview of APMC |
abstract = <nowiki>{</nowiki>In this paper, we give a brief overview of APMC |
||
(Approximate Probabilistic Model Checker). APMC is a model |
(Approximate Probabilistic Model Checker). APMC is a model |
||
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.}
}