Flow faster: efficient decision algorithms for probabilistic simulations
Abstraction techniques based on simulation relations have become an important and effective proof technique to avoid the infamous state space explosion problem. In the context of Markov chains, strong and weak simulation relations have been proposed ((B. Jonsson and K.G. Larsen, 1991), (C. Baier et al., 2002)), together with corresponding decision algorithms ((C. Baier et al., 2000), (C. Baier et al., 2004), but it is as yet unclear whether they can be used as effectively as their non-stochastic counterparts. This paper presents drastically improved algorithms to decide whether one (discrete- or continuous-time) Markov chain strongly or weakly simulates another. The key innovation is the use of parametric maximum flow techniques to amortize computations
WOS:000268642100006
2007
155
169
Event name | Event place | Event date |
Braga, Portugal | March 24 - April 1, 2007 | |