|
Computing Probability Lower and Upper Bounds for LTL Formulae over Sequential and Concurrent Markov Chains
Baier, Christel
;
Kwiatkowska, Marta
;
Norman, Gethin
|
URL:
|
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=1...
|
|
Dokumenttyp:
|
Konferenzveröffentlichung
|
|
Erscheinungsjahr:
|
1999
|
|
Buchtitel:
|
PROBMIV'98, First International Workshop on Probabilistic Methods in Verification : proceedings
|
|
Titel einer Zeitschrift oder einer Reihe:
|
Electronic Notes in Theoretical Computer Science : ENTCS
|
|
Band/Volume:
|
22
|
|
Herausgeber:
|
Baier, Christel
|
|
Ort der Veröffentlichung:
|
Amsterdam [u.a.]
|
|
Verlag:
|
Elsevier
|
|
ISSN:
|
1571-0661
|
|
Sprache der Veröffentlichung:
|
Englisch
|
|
Einrichtung:
|
Fakultät für Wirtschaftsinformatik und Wirtschaftsmathematik > Praktische Informatik II (Majster-Cederbaum -2005, Em)
|
|
Fachgebiet:
|
004 Informatik
|
|
Abstract:
|
Probabilistic verification of sequential and concurrent Markov chains against linear time specifications is known to be expensive in terms of time and space: time is exponential in the size of the formula and polynomial in the size of the state space [Var85, CY95]. This paper proposes a more efficient alternative to compute for a linear time formula only a lower and upper bound on the probability measure of the set of paths satisfying it, instead of calculating the exact probability. This yields a coarser estimate, namely an interval of values contained in [0,1] to which the actual probability belongs, but is much faster (polynomial in the size of the formula and the state space), and could thus be useful as an initial check in a model checking tool.
|
|
Zusätzliche Informationen:
|
Online Ressource
|
 | Dieser Eintrag ist Teil der Universitätsbibliographie. |
 Suche Autoren in
Sie haben einen Fehler gefunden? Teilen Sie uns Ihren Korrekturwunsch bitte hier mit: E-Mail
Actions (login required)
 |
Eintrag anzeigen |
|
|
