Three-valued abstraction for probabilistic systems
Title | Three-valued abstraction for probabilistic systems |
Publication Type | Journal Article |
Year of Publication | 2012 |
Authors | Joost-Pieter Katoen, Klink, D, Leucker, M, Wolf, V |
Journal | Journal of Algebraic and Logic Programming (JLAP) |
Volume | 81 |
Issue | 4 |
Start Page | 356 |
Pagination | 34 |
Abstract | This paper proposes a novel abstraction technique for fully probabilistic systems. The models of our study are classical discrete-time and continuous-time Markov chains (DTMCs and CTMCs, for short). A DTMC is a Kripke structure in which each transition is equipped with a discrete probability; in a CTMC, in addition, state residence times are governed by negative exponential distributions. Our abstraction technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key ingredients of our technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. It is shown that this provides a conservative abstraction for both negative and affirmative verification results for a three-valued semantics of PCTL (Probabilistic Computation Tree Logic). In the continuous-time setting, the key idea is to apply abstraction on uniform CTMCs which are readily obtained from general CTMCs. In a similar way as for the discrete case, this is shown to yield a conservative abstraction for a three-valued semantics of CSL (Continuous Stochastic Logic). Abstract CTMCs can be verified by computing time-bounded reachability probabilities in continuous-time MDPs. |
URL | http://dx.doi.org/10.1016/j.jlap.2012.03.007 |
DOI | 10.1016/j.jlap.2012.03.007 |
@article {749, title = {Three-valued abstraction for probabilistic systems}, journal = {Journal of Algebraic and Logic Programming (JLAP)}, volume = {81}, year = {2012}, pages = {34}, chapter = {356}, abstract = {This paper proposes a novel abstraction technique for fully probabilistic systems. The models of our study are classical discrete-time and continuous-time Markov chains (DTMCs and CTMCs, for short). A DTMC is a Kripke structure in which each transition is equipped with a discrete probability; in a CTMC, in addition, state residence times are governed by negative exponential distributions. Our abstraction technique fits within the realm of three-valued abstraction methods that have been used successfully for traditional model checking. The key ingredients of our technique are a partitioning of the state space combined with an abstraction of transition probabilities by intervals. It is shown that this provides a conservative abstraction for both negative and affirmative verification results for a three-valued semantics of PCTL (Probabilistic Computation Tree Logic). In the continuous-time setting, the key idea is to apply abstraction on uniform CTMCs which are readily obtained from general CTMCs. In a similar way as for the discrete case, this is shown to yield a conservative abstraction for a three-valued semantics of CSL (Continuous Stochastic Logic). Abstract CTMCs can be verified by computing time-bounded reachability probabilities in continuous-time MDPs.}, doi = {http://dx.doi.org/10.1016/j.jlap.2012.03.007}, url = {http://dx.doi.org/10.1016/j.jlap.2012.03.007}, author = {Joost-Pieter Katoen and Daniel Klink and Martin Leucker and Verena Wolf} }
- News
- Research
- Teaching
- Staff
- Martin Leucker
- Diedrich Wolter
- Ulrike Schräger-Ahrens
- Aliyu Ali
- Mahmoud Abdelrehim
- Phillip Bende
- Juljan Bouchagiar
- Marc Bätje
- Tobias Braun
- Gerhard Buntrock
- Anja Grotrian
- Hannes Hesse
- Raik Hipler
- Elaheh Hosseinkhani
- Hannes Kallwies
- Frauke Kerlin
- Karam Kharraz
- Mohammad Khodaygani
- Ludwig Pechmann
- Waqas Rehan
- Martin Sachenbacher
- Andreas Schuldei
- Annette Stümpel
- Gesina Schwalbe
- Tobias Schwartz
- Daniel Thoma
- Lars Vosteen
- Open Positions
- Contact