TY - GEN
T1 - Least upper bounds for probability measures and their applications to abstractions
AU - Chadha, Rohit
AU - Viswanathan, Mahesh
AU - Viswanathan, Ramesh
PY - 2008
Y1 - 2008
N2 - Abstraction is a key technique to combat the state space explosion problem in model checking probabilistic systems. In this paper we present new ways to abstract Discrete Time Markov Chains (DTMCs), Markov Decision Processes (MDPs), and Continuous Time Markov Chains (CTMCs). The main advantage of our abstractions is that they result in abstract models that are purely probabilistic, which maybe more amenable to automatic analysis than models with both nondeterministic and probabilistic steps that typically arise from previously known abstraction techniques. A key technical tool, developed in this paper, is the construction of least upper bounds for any collection of probability measures. This upper bound construction may be of independent interest that could be useful in the abstract interpretation and static analysis of probabilistic programs.
AB - Abstraction is a key technique to combat the state space explosion problem in model checking probabilistic systems. In this paper we present new ways to abstract Discrete Time Markov Chains (DTMCs), Markov Decision Processes (MDPs), and Continuous Time Markov Chains (CTMCs). The main advantage of our abstractions is that they result in abstract models that are purely probabilistic, which maybe more amenable to automatic analysis than models with both nondeterministic and probabilistic steps that typically arise from previously known abstraction techniques. A key technical tool, developed in this paper, is the construction of least upper bounds for any collection of probability measures. This upper bound construction may be of independent interest that could be useful in the abstract interpretation and static analysis of probabilistic programs.
UR - http://www.scopus.com/inward/record.url?scp=54249122162&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=54249122162&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-85361-9_23
DO - 10.1007/978-3-540-85361-9_23
M3 - Conference contribution
AN - SCOPUS:54249122162
SN - 354085360X
SN - 9783540853602
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 264
EP - 278
BT - CONCUR 2008 - Concurrency Theory - 19th International Conference, CONCUR 2008, Proceedings
T2 - 19th International Conference on Concurrency Theory, CONCUR 2008
Y2 - 19 August 2008 through 22 August 2008
ER -