Strong, weak and branching bisimulation for transition systems and Markov reward chains: A unifying matrix approach

N. Trcka

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)

Abstract

We first study labeled transition systems with explicit successful termination. We establish the notions of strong, weak, and branching bisimulation in terms of boolean matrix theory, introducing thus a novel and powerful algebraic apparatus. Next we consider Markov reward chains which are standardly presented in real matrix theory. By interpreting the obtained matrix conditions for bisimulations in this setting, we automatically obtain the definitions of strong, weak, and branching bisimulation for Markov reward chains. The obtained strong and weak bisimulations are shown to coincide with some existing notions, while the obtained branching bisimulation is new, but its usefulness is questionable.
Original languageEnglish
Title of host publicationProceedings First Workshop on Quantitative Formal Methods: Theory and Applications (Eindhoven, The Netherlands, November 3, 2009)
EditorsS. Andova, A. McIver, P. D'Argenio, P.J.L. Cuijpers, J. Markovski, C. Morgan, M. Núñez
Pages55-66
DOIs
Publication statusPublished - 2009

Publication series

NameElectronic Proceedings in Theoretical Computer Science
Volume13
ISSN (Print)2075-2180

Fingerprint Dive into the research topics of 'Strong, weak and branching bisimulation for transition systems and Markov reward chains: A unifying matrix approach'. Together they form a unique fingerprint.

Cite this