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 -