TY - GEN
T1 - Weighted branching systems
T2 - 16th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2018
AU - Jensen, Mathias Claus
AU - Larsen, Kim Guldstrand
AU - Mardare, Radu
PY - 2018/1/1
Y1 - 2018/1/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85053139004&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-00151-3_9
DO - 10.1007/978-3-030-00151-3_9
M3 - Article in proceeding
AN - SCOPUS:85053139004
SN - 9783030001506
T3 - Lecture Notes in Computer Science
SP - 145
EP - 161
BT - Formal Modeling and Analysis of Timed Systems
A2 - Jansen, David N.
A2 - Prabhakar, Pavithra
PB - Springer
Y2 - 4 September 2018 through 6 September 2018
ER -