Abstract
Metric labelled transition systems are labelled transition systems whose states and actions form (pseudo)metric spaces. These systems can capture a large class of timed transition systems, including systems with uncountably many states and uncountable nondeterminism. In this paper a behavioural pseudometric is introduced for metric labelled transition systems. The behavioural distance between states, a nonnegative real number, captures the similarity of the behaviour of those states. The smaller the distance, the more alike the states are. In particular, the distance between states is 0 iff they are bisimilar. Three different characterisations of this pseudometric are given: a fixed point, a logical and a coinductive characterisation. These generalise the fixed point, logical and coinductive characterisations of bisimilarity.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aczel, P., Mendler, N.: A final coalgebra theorem. In: Dybjer, P., Pitts, A.M., Pitt, D.H., Poigné, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol. 389, pp. 357–365. Springer, Heidelberg (1989)
Arbib, M.A., Manes, E.G.: Arrows, Structures, and Functors: the categorical imperative. Academic Press, London (1975)
Barr, M.: Terminal coalgebras in well-founded set theory. Theoretical Computer Science 114(2), 299–315 (1993)
van Breugel, F.: A behavioural pseudometric for metric labelled transition systems. Technical Report CS-2005-11, York University (2005)
van Breugel, F., Hermida, C., Makkai, M., Worrell, J.: An accessible approach to behavioural pseudometrics. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1018–1030. Springer, Heidelberg (2005)
van Breugel, F., Worrell, J.: An algorithm for quantitative verification of probabilistic transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 336–350. Springer, Heidelberg (2001)
van Breugel, F., Worrell, J.: Towards quantitative verification of probabilistic transition systems. In: Orejas, F., Spirakis, P.G., van Leeuwen, J. (eds.) ICALP 2001. LNCS, vol. 2076, pp. 421–432. Springer, Heidelberg (2001)
van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science 331(1), 115–142 (2005)
de Alfaro, L.: Quantitative verification and control via the mu-calculus. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 102–126. Springer, Heidelberg (2003)
de Alfaro, L., Faella, M., Stoelinga, M.: Linear and branching metrics for quantitative transition systems. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 97–109. Springer, Heidelberg (2004)
de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 1022–1037. Springer, Heidelberg (2003)
Deng, Y., Chothia, T., Palamidessi, C., Pang, J.: Metrics for action-labelled quantitative transition systems. In: Proceedings of QAPL, ENTCS. Elsevier, Amsterdam (2005)
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)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: The metric analogue of weak bisimulation for probabilistic processes. In: Proceedings of LICS, pp. 413–422. IEEE, Los Alamitos (2002)
Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theoretical Computer Science 318(3), 323–354 (2004)
Giacalone, A., Jou, C.-C., Smolka, S.A.: Algebraic reasoning for probabilistic concurrent systems. In: Proceedings of PROCOMET, pp. 443–458. North-Holland, Amsterdam (1990)
Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. Technical Report MS-CIS-05-10, University of Pennsylvania (2005)
Gupta, V., Jagadeesan, R., Panangaden, P.: Approximate reasoning for real-time probabilistic processes. In: Proceedings of QEST, pp. 304–313. IEEE, Los Alamitos (2004)
Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), 137–161 (1985)
Jacobs, B., Rutten, J.J.M.M.: A tutorial on (co)algebras and (co)induction. Bulletin of the EATCS 62, 222–259 (1997)
Makkai, M., Paré, R.: Accessible Categories: The Foundation of Categorical Model Theory. American Mathematical Society (1989)
Milner, R.: Communication and Concurrency. Prentice Hall International, Englewood Cliffs (1989)
Milner, R.: David Michael Ritchie Park (1935–1990) in memoriam. Theoretical Computer Science 133(2), 187–200 (1994)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Sangiorgi, D.: Bisimulation: from the origins to today. In: Proceedings of LICS, pp. 298–302. IEEE, Los Alamitos (2004)
Smyth, M.B.: Topology. In: Handbook of Logic in Computer Science, vol. 1, pp. 641–761. Oxford University Press, Oxford (1992)
Steffen, B., Ingólfsdóttir, A.: Characteristic formulae for processes with divergence. Information and Computation 110(1), 149–163 (1994)
Winskel, G., Nielsen, M.: Models for concurrency. In: Handbook of Logic in Computer Science, vol. 4, pp. 1–148. Oxford University Press, Oxford (1995)
Ying, M.: Bisimulation indexes and their applications. Theoretical Computer Science 275(1/2), 1–68 (2002)
Ying, M., Wirsing, M.: Approximate bisimilarity. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 309–322. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Breugel, F. (2005). A Behavioural Pseudometric for Metric Labelled Transition Systems. In: Abadi, M., de Alfaro, L. (eds) CONCUR 2005 – Concurrency Theory. CONCUR 2005. Lecture Notes in Computer Science, vol 3653. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11539452_14
Download citation
DOI: https://doi.org/10.1007/11539452_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28309-6
Online ISBN: 978-3-540-31934-4
eBook Packages: Computer ScienceComputer Science (R0)