Giorgio Bacci ; Giovanni Bacci ; Kim G. Larsen ; Radu Mardare - On-the-Fly Computation of Bisimilarity Distances

lmcs:3753 - Logical Methods in Computer Science, June 30, 2017, Volume 13, Issue 2 - https://doi.org/10.23638/LMCS-13(2:13)2017
On-the-Fly Computation of Bisimilarity DistancesArticle

Authors: 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.


    Volume: Volume 13, Issue 2
    Published on: June 30, 2017
    Accepted on: June 30, 2017
    Submitted on: June 30, 2017
    Keywords: Computer Science - Logic in Computer Science,G.3,I.1.4,I.6.4
    Funding:
      Source : OpenAIRE Graph
    • Learning, Analysis, SynthesiS and Optimization of Cyber-Physical Systems; Funder: European Commission; Code: 669844

    1 Document citing this article

    Consultation statistics

    This page has been seen 1694 times.
    This article's PDF has been downloaded 437 times.