On-the-fly exact computation of bisimilarity distances

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

28 Citations (Scopus)

Abstract

This paper proposes an algorithm for exact computation of bisimilarity distances between discrete-time Markov chains introduced by Desharnais et. al. Our work is inspired by the theoretical results presented by Chen et. al. at FoSSaCS'12, proving that these distances can be computed in polynomial time using the ellipsoid method. Despite its theoretical importance, the ellipsoid method is known to be inefficient in practice. To overcome this problem, we propose an efficient on-the-fly algorithm which, unlike other existing solutions, computes exactly the distances between given states and avoids the exhaustive state space exploration. It is parametric in a given set of states for which we want to compute the distances. Our technique successively refines 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 Markov chains shows that our algorithm improves, on average, the efficiency of the corresponding iterative algorithms with orders of magnitude.

Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems. TACAS 2013.
EditorsN. Pieterman, S.A. Smolka
Place of PublicationBerlin
PublisherSpringer-Verlag
Pages1-15
Number of pages15
ISBN (Print)9783642367410
DOIs
Publication statusPublished - 5 Mar 2013
Event19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013 - Rome, Italy
Duration: 16 Mar 201324 Mar 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7795 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013
CountryItaly
CityRome
Period16/03/1324/03/13

Fingerprint

Exact Computation
Ellipsoid Method
Markov processes
Markov chain
State Space
Approximation
Iterative Algorithm
Polynomials
Polynomial time
Discrete-time
Target

Keywords

  • Markov chain
  • discount factor
  • transportation problem
  • exact computation
  • greedy strategy

Cite this

Bacci, G., Bacci, G., Larsen, K. G., & Mardare, R. (2013). On-the-fly exact computation of bisimilarity distances. In N. Pieterman, & S. A. Smolka (Eds.), Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013. (pp. 1-15). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7795 LNCS). Berlin: Springer-Verlag. https://doi.org/10.1007/978-3-642-36742-7_1
Bacci, Giorgio ; Bacci, Giovanni ; Larsen, Kim G. ; Mardare, Radu. / On-the-fly exact computation of bisimilarity distances. Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013.. editor / N. Pieterman ; S.A. Smolka. Berlin : Springer-Verlag, 2013. pp. 1-15 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{c7a59f366d034b21aeebe6b1cdebbbe7,
title = "On-the-fly exact computation of bisimilarity distances",
abstract = "This paper proposes an algorithm for exact computation of bisimilarity distances between discrete-time Markov chains introduced by Desharnais et. al. Our work is inspired by the theoretical results presented by Chen et. al. at FoSSaCS'12, proving that these distances can be computed in polynomial time using the ellipsoid method. Despite its theoretical importance, the ellipsoid method is known to be inefficient in practice. To overcome this problem, we propose an efficient on-the-fly algorithm which, unlike other existing solutions, computes exactly the distances between given states and avoids the exhaustive state space exploration. It is parametric in a given set of states for which we want to compute the distances. Our technique successively refines 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 Markov chains shows that our algorithm improves, on average, the efficiency of the corresponding iterative algorithms with orders of magnitude.",
keywords = "Markov chain, discount factor, transportation problem, exact computation, greedy strategy",
author = "Giorgio Bacci and Giovanni Bacci and Larsen, {Kim G.} and Radu Mardare",
year = "2013",
month = "3",
day = "5",
doi = "10.1007/978-3-642-36742-7_1",
language = "English",
isbn = "9783642367410",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "1--15",
editor = "N. Pieterman and S.A. Smolka",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013.",

}

Bacci, G, Bacci, G, Larsen, KG & Mardare, R 2013, On-the-fly exact computation of bisimilarity distances. in N Pieterman & SA Smolka (eds), Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013.. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 7795 LNCS, Springer-Verlag, Berlin, pp. 1-15, 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, 16/03/13. https://doi.org/10.1007/978-3-642-36742-7_1

On-the-fly exact computation of bisimilarity distances. / Bacci, Giorgio; Bacci, Giovanni; Larsen, Kim G.; Mardare, Radu.

Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013.. ed. / N. Pieterman; S.A. Smolka. Berlin : Springer-Verlag, 2013. p. 1-15 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7795 LNCS).

Research output: Chapter in Book/Report/Conference proceedingConference contribution book

TY - GEN

T1 - On-the-fly exact computation of bisimilarity distances

AU - Bacci, Giorgio

AU - Bacci, Giovanni

AU - Larsen, Kim G.

AU - Mardare, Radu

PY - 2013/3/5

Y1 - 2013/3/5

N2 - This paper proposes an algorithm for exact computation of bisimilarity distances between discrete-time Markov chains introduced by Desharnais et. al. Our work is inspired by the theoretical results presented by Chen et. al. at FoSSaCS'12, proving that these distances can be computed in polynomial time using the ellipsoid method. Despite its theoretical importance, the ellipsoid method is known to be inefficient in practice. To overcome this problem, we propose an efficient on-the-fly algorithm which, unlike other existing solutions, computes exactly the distances between given states and avoids the exhaustive state space exploration. It is parametric in a given set of states for which we want to compute the distances. Our technique successively refines 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 Markov chains shows that our algorithm improves, on average, the efficiency of the corresponding iterative algorithms with orders of magnitude.

AB - This paper proposes an algorithm for exact computation of bisimilarity distances between discrete-time Markov chains introduced by Desharnais et. al. Our work is inspired by the theoretical results presented by Chen et. al. at FoSSaCS'12, proving that these distances can be computed in polynomial time using the ellipsoid method. Despite its theoretical importance, the ellipsoid method is known to be inefficient in practice. To overcome this problem, we propose an efficient on-the-fly algorithm which, unlike other existing solutions, computes exactly the distances between given states and avoids the exhaustive state space exploration. It is parametric in a given set of states for which we want to compute the distances. Our technique successively refines 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 Markov chains shows that our algorithm improves, on average, the efficiency of the corresponding iterative algorithms with orders of magnitude.

KW - Markov chain

KW - discount factor

KW - transportation problem

KW - exact computation

KW - greedy strategy

UR - http://www.scopus.com/inward/record.url?scp=84874447331&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-36742-7_1

DO - 10.1007/978-3-642-36742-7_1

M3 - Conference contribution book

SN - 9783642367410

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 1

EP - 15

BT - Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013.

A2 - Pieterman, N.

A2 - Smolka, S.A.

PB - Springer-Verlag

CY - Berlin

ER -

Bacci G, Bacci G, Larsen KG, Mardare R. On-the-fly exact computation of bisimilarity distances. In Pieterman N, Smolka SA, editors, Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2013.. Berlin: Springer-Verlag. 2013. p. 1-15. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-642-36742-7_1