Variable Probabilistic Abstraction Refinement
In Automated Technology for Verification and Analysis - 10th
International Symposium (ATVA)
, pages 300-316, Springer
, Lecture Notes in Computer Science 7561, 2012.
Downloads: pdf, bibURL: http://dx.doi.org/10.1007/978-3-642-33386-6_24
Abstract. 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.