Variable Probabilistic Abstraction Refinement

Luis María Ferrer Fioriti, Ernst Moritz Hahn, Holger Hermanns, Björn Wachter

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

3 Citations (Scopus)


Predicate abstraction has proven powerful in the analysis of very large probabilistic systems, but has thus far been limited to the analysis of systems with a fixed number of distinct transition probabilities. This excludes a large variety of potential analysis cases, ranging from sensor networks to biochemical systems. In these systems, transition probabilities are often given as a function of state variables—leading to an arbitrary number of different probabilities.

This paper overcomes this shortcoming. It extends existing abstraction techniques to handle such variable probabilities. We first identify the most precise abstraction in this setting, the best transformer. For practicality purposes, we then devise another type of abstraction, mapping on extensions of constraint or interval Markov chains, which is less precise but better applicable in practice. Refinement techniques are employed in case a given abstraction yields too imprecise results. We demonstrate the practical applicability of our method on two case studies.
Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Thiruvananthapuram, India, October 3-6, 2012. Proceedings
Number of pages17
Publication statusPublished - 2012
Externally publishedYes


Dive into the research topics of 'Variable Probabilistic Abstraction Refinement'. Together they form a unique fingerprint.

Cite this