Projects per year
Abstract
We propose a distance between continuoustime Markov chains (CTMCs) and study the problem of computing it by comparing three different algorithmic methodologies: iterative, linear program, and onthefly. In a work presented at FoSSaCS'12, Chen et al. characterized the bisimilarity distance of Desharnais et al. between discretetime 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 continuoustime 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 onthefly 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 overapproximations 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.
Original language  English 

Journal  Logical Methods in Computer Science 
Volume  13 
Issue number  2 
ISSN  18605974 
DOIs  
Publication status  Published  2017 
Keywords
 Markov chains
 Continuoustime Markov chains
 behavioral distances
 onthefly algorithm
 probabilistic systems
Fingerprint Dive into the research topics of 'OntheFly Computation of Bisimilarity Distances'. Together they form a unique fingerprint.
Projects
 2 Finished

IDEA4CPS: Foundations for CyberPhysical Sytems
Larsen, K. G., Skou, A., Nielsen, B., Bulychev, P., Ravn, A. P. & Poulsen, D. B.
01/04/2011 → 30/04/2015
Project: Research

MTLAB: MTLAB A VKR Foundation Center of Excellence
Larsen, K. G., Skou, A., Srba, J., Ravn, A. P., David, A. & Wisniewski, R.
01/10/2008 → 01/10/2013
Project: Research