Name
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. |
Year | DOI | Venue |
|---|---|---|
2012 | 10.1007/978-3-642-33386-6_24 | ATVA |
Keywords | Field | DocType |
potential analysis case,large probabilistic system,arbitrary number,predicate abstraction,abstraction yield,distinct transition probability,fixed number,precise abstraction,variable probabilistic abstraction refinement,case study,abstraction technique | Discrete mathematics,Abstraction,Predicate abstraction,Computer science,State function,Markov chain,Markov decision process,Algorithm,Theoretical computer science,Abstraction inversion,Probabilistic logic,Wireless sensor network | Conference |
Citations | PageRank | References |
2 | 0.38 | 17 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Luis María Ferrer Fioriti | 1 | 53 | 3.02 |
| Ernst Moritz Hahn | 2 | 368 | 23.99 |
| Holger Hermanns | 3 | 3418 | 229.22 |
| Björn Wachter | 4 | 326 | 20.09 |