The BisimDist library: efficient computation of bisimilarity distances for Markovian models

Giorgio Bacci, Giovanni Bacci, Kim Guldstrand Larsen, Radu Mardare

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

4 Citations (Scopus)

Abstract

This paper presents a library for exactly computing the bisimilarity Kantorovich-based pseudometrics between Markov chains and between Markov decision processes. These are distances that measure the behavioral discrepancies between non-bisimilar systems. They are computed by using an on-the-fly greedy strategy that prevents the exhaustive state space exploration and does not require a complete storage of the data structures. Tests performed on a consistent set of (pseudo)randomly generated instances show that our algorithm improves the efficiency of the previously proposed iterative algorithms, on average, with orders of magnitude. The tool is available as a Mathematica package library.

Original languageEnglish
Title of host publicationQuantitative Evaluation of Systems. QEST 2013
EditorsK. Joshi, M. Siegle, M. Stoelinga, P.R. D'Argenio
Place of PublicationBerlin
PublisherSpringer-Verlag
Pages278-281
Number of pages4
ISBN (Print)9783642401954
DOIs
Publication statusPublished - 28 Aug 2013
Event10th International Conference on Quantitative Evaluation of Systems, QEST 2013 - Buenos Aires, Argentina
Duration: 27 Aug 201330 Aug 2013

Publication series

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

Conference

Conference10th International Conference on Quantitative Evaluation of Systems, QEST 2013
CountryArgentina
CityBuenos Aires
Period27/08/1330/08/13

Fingerprint

Pseudometric
Markov Decision Process
Mathematica
Distance Measure
Markov processes
Iterative Algorithm
Discrepancy
Data structures
Markov chain
Data Structures
State Space
Computing
Model
Libraries
Strategy

Keywords

  • discount factor
  • Markov decision processes
  • probability transition matrix
  • greedy strategy
  • action label

Cite this

Bacci, G., Bacci, G., Guldstrand Larsen, K., & Mardare, R. (2013). The BisimDist library: efficient computation of bisimilarity distances for Markovian models. In K. Joshi, M. Siegle, M. Stoelinga, & P. R. D'Argenio (Eds.), Quantitative Evaluation of Systems. QEST 2013 (pp. 278-281). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8054 LNCS). Berlin: Springer-Verlag. https://doi.org/10.1007/978-3-642-40196-1_23
Bacci, Giorgio ; Bacci, Giovanni ; Guldstrand Larsen, Kim ; Mardare, Radu. / The BisimDist library : efficient computation of bisimilarity distances for Markovian models. Quantitative Evaluation of Systems. QEST 2013. editor / K. Joshi ; M. Siegle ; M. Stoelinga ; P.R. D'Argenio. Berlin : Springer-Verlag, 2013. pp. 278-281 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{66798e77815b4f61bd58a9d9277b6c68,
title = "The BisimDist library: efficient computation of bisimilarity distances for Markovian models",
abstract = "This paper presents a library for exactly computing the bisimilarity Kantorovich-based pseudometrics between Markov chains and between Markov decision processes. These are distances that measure the behavioral discrepancies between non-bisimilar systems. They are computed by using an on-the-fly greedy strategy that prevents the exhaustive state space exploration and does not require a complete storage of the data structures. Tests performed on a consistent set of (pseudo)randomly generated instances show that our algorithm improves the efficiency of the previously proposed iterative algorithms, on average, with orders of magnitude. The tool is available as a Mathematica package library.",
keywords = "discount factor, Markov decision processes, probability transition matrix, greedy strategy, action label",
author = "Giorgio Bacci and Giovanni Bacci and {Guldstrand Larsen}, Kim and Radu Mardare",
year = "2013",
month = "8",
day = "28",
doi = "10.1007/978-3-642-40196-1_23",
language = "English",
isbn = "9783642401954",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "278--281",
editor = "K. Joshi and M. Siegle and M. Stoelinga and P.R. D'Argenio",
booktitle = "Quantitative Evaluation of Systems. QEST 2013",

}

Bacci, G, Bacci, G, Guldstrand Larsen, K & Mardare, R 2013, The BisimDist library: efficient computation of bisimilarity distances for Markovian models. in K Joshi, M Siegle, M Stoelinga & PR D'Argenio (eds), Quantitative Evaluation of Systems. QEST 2013. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8054 LNCS, Springer-Verlag, Berlin, pp. 278-281, 10th International Conference on Quantitative Evaluation of Systems, QEST 2013, Buenos Aires, Argentina, 27/08/13. https://doi.org/10.1007/978-3-642-40196-1_23

The BisimDist library : efficient computation of bisimilarity distances for Markovian models. / Bacci, Giorgio; Bacci, Giovanni; Guldstrand Larsen, Kim; Mardare, Radu.

Quantitative Evaluation of Systems. QEST 2013. ed. / K. Joshi; M. Siegle; M. Stoelinga; P.R. D'Argenio. Berlin : Springer-Verlag, 2013. p. 278-281 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8054 LNCS).

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

TY - GEN

T1 - The BisimDist library

T2 - efficient computation of bisimilarity distances for Markovian models

AU - Bacci, Giorgio

AU - Bacci, Giovanni

AU - Guldstrand Larsen, Kim

AU - Mardare, Radu

PY - 2013/8/28

Y1 - 2013/8/28

N2 - This paper presents a library for exactly computing the bisimilarity Kantorovich-based pseudometrics between Markov chains and between Markov decision processes. These are distances that measure the behavioral discrepancies between non-bisimilar systems. They are computed by using an on-the-fly greedy strategy that prevents the exhaustive state space exploration and does not require a complete storage of the data structures. Tests performed on a consistent set of (pseudo)randomly generated instances show that our algorithm improves the efficiency of the previously proposed iterative algorithms, on average, with orders of magnitude. The tool is available as a Mathematica package library.

AB - This paper presents a library for exactly computing the bisimilarity Kantorovich-based pseudometrics between Markov chains and between Markov decision processes. These are distances that measure the behavioral discrepancies between non-bisimilar systems. They are computed by using an on-the-fly greedy strategy that prevents the exhaustive state space exploration and does not require a complete storage of the data structures. Tests performed on a consistent set of (pseudo)randomly generated instances show that our algorithm improves the efficiency of the previously proposed iterative algorithms, on average, with orders of magnitude. The tool is available as a Mathematica package library.

KW - discount factor

KW - Markov decision processes

KW - probability transition matrix

KW - greedy strategy

KW - action label

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

U2 - 10.1007/978-3-642-40196-1_23

DO - 10.1007/978-3-642-40196-1_23

M3 - Conference contribution book

AN - SCOPUS:84882796373

SN - 9783642401954

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

SP - 278

EP - 281

BT - Quantitative Evaluation of Systems. QEST 2013

A2 - Joshi, K.

A2 - Siegle, M.

A2 - Stoelinga, M.

A2 - D'Argenio, P.R.

PB - Springer-Verlag

CY - Berlin

ER -

Bacci G, Bacci G, Guldstrand Larsen K, Mardare R. The BisimDist library: efficient computation of bisimilarity distances for Markovian models. In Joshi K, Siegle M, Stoelinga M, D'Argenio PR, editors, Quantitative Evaluation of Systems. QEST 2013. Berlin: Springer-Verlag. 2013. p. 278-281. (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-40196-1_23