Distribution, approximation and probabilistic model checking

From LRDE

Abstract

APMC is a model checker dedicated to the quantitative verification of fully probabilistic systems against LTL formulas. Using a Monte-Carlo method in order to efficiently approximate the verification of probabilistic specifications, it could be used naturally in a distributed framework. We present here the tool and his distribution scheme, together with extensive performance evaluationshowing the scalability of the method, even on clusters containing 500+ heterogeneous workstations.


Bibtex (lrde.bib)

@InProceedings{	  guirado.05.pdmc,
  author	= {Guillaume Guirado and Thomas Herault and Richard Lassaigne
		  and Sylvain Peyronnet},
  title		= {Distribution, approximation and probabilistic model
		  checking},
  booktitle	= {Proceedings of the 4th international workshop on Parallel
		  and Distributed Model Checking (PDMC)},
  year		= 2005,
  abstract	= {APMC is a model checker dedicated to the quantitative
		  verification of fully probabilistic systems against LTL
		  formulas. Using a Monte-Carlo method in order to
		  efficiently approximate the verification of probabilistic
		  specifications, it could be used naturally in a distributed
		  framework. We present here the tool and his distribution
		  scheme, together with extensive performance evaluation,
		  showing the scalability of the method, even on clusters
		  containing 500+ heterogeneous workstations.}
}