Probabilistic verification and approximation

From LRDE

The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.

Abstract

Model checking is an algorithmic method allowing to automatically verify if a system which is represented as a Kripke model satisfies a given specification. Specifications are usually expressed by formulas of temporal logic. The first objective of this paper is to give an overview of methods able to verify probabilistic systems. Models of such systems are labelled discrete time Markov chains and specifications are expressed in extensions of temporal logic by probabilistic operators. The second objective is to focus on complexity of these methods and to answer the question: can probabilistic verification be efficiently approximated? In general, the answer is negative. However, in many applications, the specification formulas can be expressed in some positive fragment of linear time temporal logic. In this paper, we show how some simple randomized approximation algorithms can improve the efficiency of the verification of such probabilistic specifications.


Bibtex (lrde.bib)

@InProceedings{	  lassaigne.05.wollic,
  author	= {Richard Lassaigne and Sylvain Peyronnet},
  title		= {Probabilistic verification and approximation},
  booktitle	= {Proceedings of 12th Workshop on Logic, Language,
		  Information and Computation (Wollic)},
  year		= 2005,
  series	= {Electronic Notes in Theoretical Computer Science},
  volume	= 143,
  pages		= {101--114},
  abstract	= {Model checking is an algorithmic method allowing to
		  automatically verify if a system which is represented as a
		  Kripke model satisfies a given specification.
		  Specifications are usually expressed by formulas of
		  temporal logic. The first objective of this paper is to
		  give an overview of methods able to verify probabilistic
		  systems. Models of such systems are labelled discrete time
		  Markov chains and specifications are expressed in
		  extensions of temporal logic by probabilistic operators.
		  The second objective is to focus on complexity of these
		  methods and to answer the question: can probabilistic
		  verification be efficiently approximated? In general, the
		  answer is negative. However, in many applications, the
		  specification formulas can be expressed in some positive
		  fragment of linear time temporal logic. In this paper, we
		  show how some simple randomized approximation algorithms
		  can improve the efficiency of the verification of such
		  probabilistic specifications.}
}