On-the-Fly Computation of Bisimilarity Distances

We propose a distance between continuous-time Markov chains (CTMCs) and studythe problem of computing it by comparing three different algorithmicmethodologies: iterative, linear program, and on-the-fly. In a work presentedat FoSSaCS'12, Chen et al. characterized the bisimilarity distance ofDesharnais et al. between discrete-time Markov chains as an optimal solution ofa linear program that can be solved by using the ellipsoid method. Inspired bytheir result, we propose a novel linear program characterization to compute thedistance in the continuous-time setting. Differently from previous proposals,ours has a number of constraints that is bounded by a polynomial in the size ofthe CTMC. This, in particular, proves that the distance we propose can becomputed in polynomial time. Despite its theoretical importance, the proposedlinear program characterization turns out to be inefficient in practice.Nevertheless, driven by the encouraging results of our previous work presentedat TACAS'13, we propose an efficient on-the-fly algorithm, which, unlike theother mentioned solutions, computes the distances between two given statesavoiding an exhaustive exploration of the state space. This technique works bysuccessively refining over-approximations of the target distances using agreedy strategy, which ensures that the state space is further explored onlywhen the current approximations are improved. Tests performed on a consistentset of (pseudo)randomly generated CTMCs show that our algorithm improves, onaverage, the efficiency of the corresponding iterative and linear programmethods with orders of magnitude