@inproceedings{a9d7422ade75440990721811850208ac,
title = "Weighted branching systems: behavioural equivalence, behavioural distance, and their logical characterisations",
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.",
keywords = "branching bisimulation, weighted branching",
author = "Jensen, {Mathias Claus} and Larsen, {Kim Guldstrand} and Radu Mardare",
year = "2018",
month = aug,
day = "26",
doi = "10.1007/978-3-030-00151-3_9",
language = "English",
isbn = "9783030001506",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "145--161",
editor = "Jansen, {David N.} and Pavithra Prabhakar",
booktitle = "Formal Modeling and Analysis of Timed Systems - 16th International Conference, FORMATS 2018, Proceedings",
note = "16th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2018 ; Conference date: 04-09-2018 Through 06-09-2018",
}