Difference between revisions of "Publications/lassaigne.05.wollic"
From LRDE
(5 intermediate revisions by the same user not shown) | |||
Line 1: | Line 1: | ||
{{Publication |
{{Publication |
||
− | | |
+ | | published = true |
+ | | date = 2005-04-11 |
||
| authors = Richard Lassaigne, Sylvain Peyronnet |
| authors = Richard Lassaigne, Sylvain Peyronnet |
||
| title = Probabilistic verification and approximation |
| title = Probabilistic verification and approximation |
||
Line 7: | Line 8: | ||
| volume = 143 |
| volume = 143 |
||
| pages = 101 to 114 |
| pages = 101 to 114 |
||
− | | project = APMC |
||
− | | 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. |
||
| lrdeprojects = APMC |
| lrdeprojects = 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. |
||
+ | | lrdenewsdate = 2005-04-11 |
||
| type = inproceedings |
| type = inproceedings |
||
| id = lassaigne.05.wollic |
| id = lassaigne.05.wollic |
||
Line 23: | Line 23: | ||
volume = 143, |
volume = 143, |
||
pages = <nowiki>{</nowiki>101--114<nowiki>}</nowiki>, |
pages = <nowiki>{</nowiki>101--114<nowiki>}</nowiki>, |
||
− | project = <nowiki>{</nowiki>APMC<nowiki>}</nowiki>, |
||
abstract = <nowiki>{</nowiki>Model checking is an algorithmic method allowing to |
abstract = <nowiki>{</nowiki>Model checking is an algorithmic method allowing to |
||
automatically verify if a system which is represented as a |
automatically verify if a system which is represented as a |
||
Line 41: | Line 40: | ||
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> |
||
Latest revision as of 18:57, 4 January 2018
- Authors
- Richard Lassaigne, Sylvain Peyronnet
- Where
- Proceedings of 12th Workshop on Logic, LanguageInformation and Computation (Wollic)
- Type
- inproceedings
- Projects
- APMC
- Date
- 2005-04-11
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.} }