Least upper bounds for probability measures and their applications to abstractions

Rohit Chadha, Mahesh Viswanathan, Ramesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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.

Original languageEnglish (US)
Title of host publicationCONCUR 2008 - Concurrency Theory - 19th International Conference, CONCUR 2008, Proceedings
Number of pages15
StatePublished - 2008
Event19th International Conference on Concurrency Theory, CONCUR 2008 - Toronto, ON, Canada
Duration: Aug 19 2008Aug 22 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5201 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Other19th International Conference on Concurrency Theory, CONCUR 2008
CityToronto, ON

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Least upper bounds for probability measures and their applications to abstractions'. Together they form a unique fingerprint.

Cite this