Compositional Abstraction for Stochastic Systems
Joost-Pieter Katoen, Daniel Klink, Martin Neuh�u�er
AIB 2009-15
We propose to exploit three-valued abstraction to stochastic systems in
a compositional way. This combines the strengths of an aggressive
state-based abstraction technique with compositional modeling. Applying
this principle to interactive Markov chains yields abstract models that
combine interval Markov chains and modal transition systems in a natural
and orthogonal way. We prove the correctness of our technique for
parallel and symmetric composition and show that it yields lower bounds
for minimal and upper bounds for maximal timed reachability
probabilities.