Skip to main content

A Behavioural Pseudometric for Metric Labelled Transition Systems

  • Conference paper
CONCUR 2005 – Concurrency Theory (CONCUR 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3653))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)

    Google Scholar 

  2. Arbib, M.A., Manes, E.G.: Arrows, Structures, and Functors: the categorical imperative. Academic Press, London (1975)

    MATH  Google Scholar 

  3. Barr, M.: Terminal coalgebras in well-founded set theory. Theoretical Computer Science 114(2), 299–315 (1993)

    Article  MATH  MathSciNet  Google Scholar 

  4. van Breugel, F.: A behavioural pseudometric for metric labelled transition systems. Technical Report CS-2005-11, York University (2005)

    Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. 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)

    Chapter  Google Scholar 

  7. 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)

    Chapter  Google Scholar 

  8. van Breugel, F., Worrell, J.: A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science 331(1), 115–142 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  9. 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)

    Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. 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)

    Chapter  Google Scholar 

  12. Deng, Y., Chothia, T., Palamidessi, C., Pang, J.: Metrics for action-labelled quantitative transition systems. In: Proceedings of QAPL, ENTCS. Elsevier, Amsterdam (2005)

    Google Scholar 

  13. 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)

    Google Scholar 

  14. 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)

    Google Scholar 

  15. Desharnais, J., Gupta, V., Jagadeesan, R., Panangaden, P.: Metrics for labelled Markov processes. Theoretical Computer Science 318(3), 323–354 (2004)

    Article  MATH  MathSciNet  Google Scholar 

  16. 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)

    Google Scholar 

  17. Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. Technical Report MS-CIS-05-10, University of Pennsylvania (2005)

    Google Scholar 

  18. Gupta, V., Jagadeesan, R., Panangaden, P.: Approximate reasoning for real-time probabilistic processes. In: Proceedings of QEST, pp. 304–313. IEEE, Los Alamitos (2004)

    Google Scholar 

  19. Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. Journal of the ACM 32(1), 137–161 (1985)

    Article  MATH  MathSciNet  Google Scholar 

  20. Jacobs, B., Rutten, J.J.M.M.: A tutorial on (co)algebras and (co)induction. Bulletin of the EATCS 62, 222–259 (1997)

    MATH  Google Scholar 

  21. Makkai, M., Paré, R.: Accessible Categories: The Foundation of Categorical Model Theory. American Mathematical Society (1989)

    Google Scholar 

  22. Milner, R.: Communication and Concurrency. Prentice Hall International, Englewood Cliffs (1989)

    MATH  Google Scholar 

  23. Milner, R.: David Michael Ritchie Park (1935–1990) in memoriam. Theoretical Computer Science 133(2), 187–200 (1994)

    Article  MathSciNet  Google Scholar 

  24. Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  25. Sangiorgi, D.: Bisimulation: from the origins to today. In: Proceedings of LICS, pp. 298–302. IEEE, Los Alamitos (2004)

    Google Scholar 

  26. Smyth, M.B.: Topology. In: Handbook of Logic in Computer Science, vol. 1, pp. 641–761. Oxford University Press, Oxford (1992)

    Google Scholar 

  27. Steffen, B., Ingólfsdóttir, A.: Characteristic formulae for processes with divergence. Information and Computation 110(1), 149–163 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  28. Winskel, G., Nielsen, M.: Models for concurrency. In: Handbook of Logic in Computer Science, vol. 4, pp. 1–148. Oxford University Press, Oxford (1995)

    Google Scholar 

  29. Ying, M.: Bisimulation indexes and their applications. Theoretical Computer Science 275(1/2), 1–68 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  30. Ying, M., Wirsing, M.: Approximate bisimilarity. In: Rus, T. (ed.) AMAST 2000. LNCS, vol. 1816, pp. 309–322. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints 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)

Publish with us

Policies and ethics