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 \(s \xrightarrow {w} s'\) to be matched by finite paths that accumulate a weight within the interval \([\frac{w}{\varepsilon }, w\varepsilon ]\), where \(\varepsilon \) 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.
This paper is based upon unpublished ideas by Foshammer et al. [FLMX17] and the 9th semester project report [Jen18] in Computer Science by the first author at Aalborg University.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115–131 (1988)
Buchholz, P., Kemper, P.: Model checking for a class of weighted automata. Discret. Event Dyn. Syst. 20(1), 103–137 (2010)
Blackburn, P., van Benthem, J.F.A.K., Wolter, F.: Handbook of Modal Logic, vol. 3. Elsevier, Amsterdam (2006)
Christoffersen, P., Hansen, M., Mariegaard, A., Ringsmose, J.T., Larsen, K.G., Mardare, R.: Parametric verification of weighted systems. In: André, É., Frehse, G. (eds.) 2nd International Workshop on Synthesis of Complex Parameters, SynCoP 2015, 11 April 2015, London, United Kingdom. OA-SICS, vol. 44, pp. 77–90. SchlossDagstuhl - Leibniz-Zentrum fuer Informatik (2015)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labeled Markov systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 258–273. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48320-9_19
De Nicola, R., Vaandrager, F.W.: Three logics for branching bisimulation. J. ACM 42(2), 458–487 (1995)
Foshammer, L., Larsen, K.G., Mariegaard, A.: Weighted branching simulation distance for parametric weighted Kripke structures. EPTCS 220, 63–75 (2016)
Foshammer, L., Larsen, K.G., Mardare, R., Xue, B.: Logical characterization and complexity of weighted branching preorders and distances. Unpublished Draft (2017)
Fahrenberg, U., Thrane, C.R., Larsen, K.G.: Distances for weighted transition systems: games and properties. EPTCS 57, 134–147 (2011)
Giacalone, A., Jou, C.-C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of the IFIP TC2 Working Conference on Programming Concepts and Methods. Citeseer (1990)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)
Jensen, M.C.: Weighted branching systems: behavioural equivalence, metric structure, and their characterisations. Technical report, 9th Semester Report at Aalborg University (2018)
Jensen, J.F., Larsen, K.G., Srba, J., Oestergaard, L.K.: Efficient model-checking of weighted CTL with upper-bound constraints. Int. J. Softw. Tools Technol. Transfer 18, 409–426 (2016)
Larsen, K.G., Fahrenberg, U., Thrane, C.R.: Metrics for weighted transition systems: axiomatization and complexity. Theor. Comput. Sci. 412(28), 3358–3369 (2011)
Larsen, K.G., Mardare, R., Panangaden, P.: Taking it to the limit: approximate reasoning for Markov processes. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 681–692. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32589-2_59
Milner, R. (ed.): A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980). https://doi.org/10.1007/3-540-10235-3
Nykänen, M., Ukkonen, E.: The exact path length problem. J. Algorithms 42(1), 41–53 (2002)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981). https://doi.org/10.1007/BFb0017309
Thrane, C., Fahrenberg, U., Larsen, K.G.: Quantitative analysis of weighted transition systems. J. Log. Algebr. Program. 79(7), 689–703 (2010)
van Glabbeek, R.J., Weijland, W.P.,: Branching time and abstraction in bisimulation semantics (extended abstract). In: IFIP Congress, pp. 613–618 (1989)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
1 Electronic supplementary material
Below is the link to the electronic supplementary material.
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Jensen, M.C., Larsen, K.G., Mardare, R. (2018). Weighted Branching Systems: Behavioural Equivalence, Behavioural Distance, and Their Logical Characterisations. In: Jansen, D., Prabhakar, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2018. Lecture Notes in Computer Science(), vol 11022. Springer, Cham. https://doi.org/10.1007/978-3-030-00151-3_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-00151-3_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-00150-6
Online ISBN: 978-3-030-00151-3
eBook Packages: Computer ScienceComputer Science (R0)