Difference between revisions of "Publications/lassaigne.05.wollic"
From LRDE
(Created page with "{{Publication | date = 2005-01-01 | authors = Richard Lassaigne, Sylvain Peyronnet | title = Probabilistic verification and approximation | booktitle = Proceedings of 12th Wor...") |
|||
Line 10: | Line 10: | ||
| urllrde = 200507-Wollic |
| urllrde = 200507-Wollic |
||
| 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. |
| 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. |
||
+ | | lrdeprojects = APMC |
||
| type = inproceedings |
| type = inproceedings |
||
| id = lassaigne.05.wollic |
| id = lassaigne.05.wollic |
||
Line 40: | Line 41: | ||
show how some simple randomized approximation algorithms |
show how some simple randomized approximation algorithms |
||
can improve the efficiency of the verification of such |
can improve the efficiency of the verification of such |
||
− | probabilistic specifications.<nowiki>}</nowiki> |
+ | probabilistic specifications.<nowiki>}</nowiki>, |
+ | lrdeprojects = <nowiki>{</nowiki>APMC<nowiki>}</nowiki> |
||
<nowiki>}</nowiki> |
<nowiki>}</nowiki> |
||
Revision as of 18:07, 4 November 2013
- Authors
- Richard Lassaigne, Sylvain Peyronnet
- Where
- Proceedings of 12th Workshop on Logic, LanguageInformation and Computation (Wollic)
- Type
- inproceedings
- Projects
- APMC
- Date
- 2005-01-01
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}, project = {APMC}, 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.}, lrdeprojects = {APMC} }