Publications/herault.06.qest

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.}
}