Variable probabilistic abstraction refinement

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

3 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 10th International Symposium, ATVA 2012, Proceedings
Pages300-316
Number of pages17
DOIs
Publication statusPublished - 2012
Externally publishedYes
Event10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012 - Thiruvananthapuram, India
Duration: 3 Oct 20126 Oct 2012
Conference number: 10

Publication series

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

Conference

Conference10th International Symposium on Automated Technology for Verification and Analysis, ATVA 2012
Abbreviated titleATVA
CountryIndia
CityThiruvananthapuram
Period3/10/126/10/12

Fingerprint Dive into the research topics of 'Variable probabilistic abstraction refinement'. Together they form a unique fingerprint.

Cite this