eng
episciences.org
Logical Methods in Computer Science
1860-5974
2017-06-30
Volume 13, Issue 2
10.23638/LMCS-13(2:13)2017
3753
journal article
On-the-Fly Computation of Bisimilarity Distances
Giorgio Bacci
Giovanni Bacci
Kim G. Larsen
Radu Mardare
We propose a distance between continuous-time Markov chains (CTMCs) and study
the problem of computing it by comparing three different algorithmic
methodologies: iterative, linear program, and on-the-fly. In a work presented
at FoSSaCS'12, Chen et al. characterized the bisimilarity distance of
Desharnais et al. between discrete-time Markov chains as an optimal solution of
a linear program that can be solved by using the ellipsoid method. Inspired by
their result, we propose a novel linear program characterization to compute the
distance in the continuous-time setting. Differently from previous proposals,
ours has a number of constraints that is bounded by a polynomial in the size of
the CTMC. This, in particular, proves that the distance we propose can be
computed in polynomial time. Despite its theoretical importance, the proposed
linear program characterization turns out to be inefficient in practice.
Nevertheless, driven by the encouraging results of our previous work presented
at TACAS'13, we propose an efficient on-the-fly algorithm, which, unlike the
other mentioned solutions, computes the distances between two given states
avoiding an exhaustive exploration of the state space. This technique works by
successively refining over-approximations of the target distances using a
greedy strategy, which ensures that the state space is further explored only
when the current approximations are improved. Tests performed on a consistent
set of (pseudo)randomly generated CTMCs show that our algorithm improves, on
average, the efficiency of the corresponding iterative and linear program
methods with orders of magnitude.
https://lmcs.episciences.org/3753/pdf
Computer Science - Logic in Computer Science
G.3
I.1.4
I.6.4