Three-valued abstraction for probabilistic systems. Katoen, J., Klink, D., Leucker, M., & Wolf, V. Journal of Logic and Algebraic Programming, 2012. doi abstract bibtex 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. © 2012 Elsevier Inc. All rights reserved.
@article{
title = {Three-valued abstraction for probabilistic systems},
type = {article},
year = {2012},
volume = {81},
id = {eba1888c-f7dc-3ecf-8674-1548423fe610},
created = {2017-01-02T09:34:04.000Z},
file_attached = {false},
profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},
last_modified = {2017-03-22T13:51:34.979Z},
read = {false},
starred = {false},
authored = {true},
confirmed = {false},
hidden = {false},
private_publication = {false},
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. © 2012 Elsevier Inc. All rights reserved.},
bibtype = {article},
author = {Katoen, J.-P. and Klink, D. and Leucker, M. and Wolf, V.},
doi = {10.1016/j.jlap.2012.03.007},
journal = {Journal of Logic and Algebraic Programming},
number = {4}
}
Downloads: 0
{"_id":"9KiA2roQM7QrrRk7L","bibbaseid":"katoen-klink-leucker-wolf-threevaluedabstractionforprobabilisticsystems-2012","downloads":0,"creationDate":"2016-02-15T09:20:58.549Z","title":"Three-valued abstraction for probabilistic systems","author_short":["Katoen, J.","Klink, D.","Leucker, M.","Wolf, V."],"year":2012,"bibtype":"article","biburl":"https://bibbase.org/service/mendeley/bbb99b2d-2278-3254-820f-2de6d915ce63","bibdata":{"title":"Three-valued abstraction for probabilistic systems","type":"article","year":"2012","volume":"81","id":"eba1888c-f7dc-3ecf-8674-1548423fe610","created":"2017-01-02T09:34:04.000Z","file_attached":false,"profile_id":"bbb99b2d-2278-3254-820f-2de6d915ce63","last_modified":"2017-03-22T13:51:34.979Z","read":false,"starred":false,"authored":"true","confirmed":false,"hidden":false,"private_publication":false,"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. © 2012 Elsevier Inc. All rights reserved.","bibtype":"article","author":"Katoen, J.-P. and Klink, D. and Leucker, M. and Wolf, V.","doi":"10.1016/j.jlap.2012.03.007","journal":"Journal of Logic and Algebraic Programming","number":"4","bibtex":"@article{\n title = {Three-valued abstraction for probabilistic systems},\n type = {article},\n year = {2012},\n volume = {81},\n id = {eba1888c-f7dc-3ecf-8674-1548423fe610},\n created = {2017-01-02T09:34:04.000Z},\n file_attached = {false},\n profile_id = {bbb99b2d-2278-3254-820f-2de6d915ce63},\n last_modified = {2017-03-22T13:51:34.979Z},\n read = {false},\n starred = {false},\n authored = {true},\n confirmed = {false},\n hidden = {false},\n private_publication = {false},\n 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. © 2012 Elsevier Inc. All rights reserved.},\n bibtype = {article},\n author = {Katoen, J.-P. and Klink, D. and Leucker, M. and Wolf, V.},\n doi = {10.1016/j.jlap.2012.03.007},\n journal = {Journal of Logic and Algebraic Programming},\n number = {4}\n}","author_short":["Katoen, J.","Klink, D.","Leucker, M.","Wolf, V."],"biburl":"https://bibbase.org/service/mendeley/bbb99b2d-2278-3254-820f-2de6d915ce63","bibbaseid":"katoen-klink-leucker-wolf-threevaluedabstractionforprobabilisticsystems-2012","role":"author","urls":{},"metadata":{"authorlinks":{"wolf, v":"https://mosi.uni-saarland.de/research/"}},"downloads":0},"search_terms":["three","valued","abstraction","probabilistic","systems","katoen","klink","leucker","wolf"],"keywords":[],"authorIDs":["6TtMsgho6wSDppwNh"],"dataSources":["me3WD7pwWySxCKW8s","ya2CyA73rpZseyrZ8"]}