Difference between revisions of "Publications/herault.06.qest"

From LRDE

(Created page with "{{Publication | date = 2006-01-01 | authors = Thomas Hérault, Richard Lassaigne, Sylvain Peyronnet | title = APMC 3.0: Approximate verification of Discrete and Continuous Tim...")
 
 
(5 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
+
| lrdeprojects = 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.
 
| 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
Line 19: 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

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