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

Keywords

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

Fingerprint Dive into the research topics of 'The BisimDist library: efficient computation of bisimilarity distances for Markovian models'. Together they form a unique fingerprint.

Cite this