Weighted branching systems: behavioural equivalence, behavioural distance, and their logical characterisations

Mathias Claus Jensen, Kim Guldstrand Larsen, Radu Mardare

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

1 Citation (Scopus)

Abstract

In this work, we extend the notion of branching bisimulation to weighted systems. We abstract away from singular transitions and allow for bisimilar systems to match each other using finite paths of similar behaviour and weight. We show that this weighted branching bisimulation is characterised by a weighted temporal logic. Due to the restrictive nature of quantitative behavioural equivalences, we develop a notion of relative distance between weighted processes by relaxing our bisimulation by some factor. Intuitively, we allow for transitions (formula presented) to be matched by finite paths that accumulate a weight within the interval (formula presented), where ε is the factor of relaxation. We extend this relaxation to our logic and show that for a class of formulae, our relaxed logic characterises our relaxed bisimulation. From this notion of relaxed bisimulation, we derive a relative pseudometric and prove robustness results. Lastly, we prove certain topological properties for classes of formulae on the open-ball topology induced by our pseudometric.

Original languageEnglish
Title of host publicationFormal Modeling and Analysis of Timed Systems - 16th International Conference, FORMATS 2018, Proceedings
EditorsDavid N. Jansen, Pavithra Prabhakar
Place of PublicationCham
PublisherSpringer-Verlag
Pages145-161
Number of pages17
ISBN (Print)9783030001506
DOIs
Publication statusPublished - 26 Aug 2018
Event16th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2018 - Beijing, China
Duration: 4 Sep 20186 Sep 2018

Publication series

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

Conference

Conference16th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2018
CountryChina
CityBeijing
Period4/09/186/09/18

    Fingerprint

Keywords

  • branching bisimulation
  • weighted branching

Cite this

Jensen, M. C., Larsen, K. G., & Mardare, R. (2018). Weighted branching systems: behavioural equivalence, behavioural distance, and their logical characterisations. In D. N. Jansen, & P. Prabhakar (Eds.), Formal Modeling and Analysis of Timed Systems - 16th International Conference, FORMATS 2018, Proceedings (pp. 145-161). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11022 LNCS). Cham: Springer-Verlag. https://doi.org/10.1007/978-3-030-00151-3_9