iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://doi.org/10.4230/LIPIcs.CONCUR.2023.38
Contextual Behavioural Metrics
Document Open Access Logo

Contextual Behavioural Metrics

Authors Ugo Dal Lago , Maurizio Murgia

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.38.pdf
  • Filesize: 1.03 MB
  • 17 pages

Document Identifiers

Author Details

Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France
Maurizio Murgia
  • Gran Sasso Science Institute, L'Aquila, Italy

Funding

The first author is supported by the ERC CoG "DIAPASoN", GA 818616, and by PNRR - M4C2 - I1.4 Project CN00000013 "National Centre for HPC, Big Data and Quantum Computing". The second author is supported by MUR project PON REACT EU DM 1062/21.

Acknowledgements

We thank the anonymous reviewers for their feedback.

Cite As Get BibTex

Ugo Dal Lago and Maurizio Murgia. Contextual Behavioural Metrics. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 38:1-38:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CONCUR.2023.38

Abstract

We introduce contextual behavioural metrics (CBMs) as a novel way of measuring the discrepancy in behaviour between processes, taking into account both quantitative aspects and contextual information. This way, process distances by construction take the environment into account: two (non-equivalent) processes may still exhibit very similar behaviour in some contexts, e.g., when certain actions are never performed. We first show how CBMs capture many well-known notions of equivalence and metric, including Larsen’s environmental parametrized bisimulation. We then study compositional properties of CBMs with respect to some common process algebraic operators, namely prefixing, restriction, non-deterministic sum, parallel composition and replication.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program reasoning
  • Theory of computation → Process calculi
Keywords
  • Behavioural metrics
  • Labelled Transition Systems
  • Differential Semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. S. Abramsky. The lazy λ-calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65-117. Addison Wesley, 1990. Google Scholar
  2. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. Computing behavioral distances, compositionally. In Proc. of MFCS, volume 8087 of Lecture Notes in Computer Science, pages 74-85. Springer, 2013. Google Scholar
  3. Harsh Beohar, Barbara König, Sebastian Küpper, and Alexandra Silva. Conditional transition systems with upgrades. Sci. Comput. Program., 186, 2020. Google Scholar
  4. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized bisimulation metrics. In Proc. of CONCUR, volume 8704 of Lecture Notes in Computer Science, pages 32-46. Springer, 2014. Google Scholar
  5. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching metrics for quantitative transition systems. In Proc. of ICALP, volume 3142 of Lecture Notes in Computer Science, pages 97-109. Springer, 2004. Google Scholar
  6. Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata, and Ikram Cherigui. A semantic account of metric preservation. In Proc. of POPL, pages 545-556. ACM, 2017. Google Scholar
  7. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labeled markov systems. In Proc. of CONCUR, volume 1664 of LNCS, pages 258-273. Springer, 1999. Google Scholar
  8. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled markov processes. Theor. Comput. Sci., 318(3):323-354, 2004. Google Scholar
  9. Josée Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proc. of LICS, pages 413-422. IEEE Computer Society, 2002. Google Scholar
  10. Josée Desharnais, François Laviolette, and Mathieu Tracol. Approximate analysis of probabilistic processes: Logic, simulation and games. In Proc. of QEST, pages 264-273. IEEE Computer Society, 2008. Google Scholar
  11. Wenjie Du, Yuxin Deng, and Daniel Gebler. Behavioural pseudometrics for nondeterministic probabilistic systems. In Proc. of SETTA, volume 9984 of Lecture Notes in Computer Science, pages 67-84, 2016. Google Scholar
  12. Wenjie Du, Yuxin Deng, and Daniel Gebler. Behavioural pseudometrics for nondeterministic probabilistic systems. Sci. Ann. Comput. Sci., 32(2):211-254, 2022. Google Scholar
  13. Norm Ferns, Prakash Panangaden, and Doina Precup. Metrics for finite markov decision processes. In Proc. of AAAI, pages 950-951. AAAI Press / The MIT Press, 2004. Google Scholar
  14. Daniel Gebler, Kim G. Larsen, and Simone Tini. Compositional bisimulation metric reasoning with probabilistic process calculi. Log. Methods Comput. Sci., 12(4), 2016. Google Scholar
  15. Daniel Gebler, Kim Guldstrand Larsen, and Simone Tini. Compositional metric reasoning with probabilistic process calculi. In Proc. of FoSSaCS, volume 9034 of Lecture Notes in Computer Science, pages 230-245. Springer, 2015. Google Scholar
  16. Daniel Gebler and Simone Tini. SOS specifications for uniformly continuous operators. J. Comput. Syst. Sci., 92:113-151, 2018. Google Scholar
  17. Guillaume Geoffroy and Paolo Pistone. A partial metric semantics of higher-order types and approximate program transformations. In Proc. of CSL, volume 183 of LIPIcs, pages 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  18. Matthew Hennessy and Huimin Lin. Symbolic bisimulations. Theor. Comput. Sci., 138(2):353-389, 1995. Google Scholar
  19. C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666-677, 1978. Google Scholar
  20. Mathias Hülsbusch and Barbara König. Deriving bisimulation congruences for conditional reactive systems. In Proc. of FoSSaCS, volume 7213 of Lecture Notes in Computer Science, pages 361-375. Springer, 2012. Google Scholar
  21. Mathias Hülsbusch, Barbara König, Sebastian Küpper, and Lars Stoltenow. Conditional bisimilarity for reactive systems. In Proc. of FSCD, volume 167 of LIPIcs, pages 10:1-10:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  22. Ugo Dal Lago, Francesco Gavazzo, and Akira Yoshimizu. Differential logical relations, part I: the simply-typed case. In Proc. of ICALP, volume 132 of LIPIcs, pages 111:1-111:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  23. Kim Guldstrand Larsen. A context dependent equivalence between processes. Theor. Comput. Sci., 49:184-215, 1987. Google Scholar
  24. F. William Lawvere. Metric spaces, generalized logic, and closed categories. In Rend. Sem. Mat. Fis. Milano, volume 43, pages 135-166, 1973. Google Scholar
  25. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. Google Scholar
  26. Robin Milner. Communication and concurrency. PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  27. David Park. Concurrency and automata on infinite sequences. In Theoretical Computer Science, pages 167-183, 1981. Google Scholar
  28. Paolo Pistone. On generalized metric spaces for the simply typed lambda-calculus. In Proc. of LICS, pages 1-14. IEEE, 2021. Google Scholar
  29. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method, pages 233-289. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2011. URL: https://doi.org/10.1017/CBO9780511792588.007.
  30. Jason Reed and Benjamin C. Pierce. Distance makes the types grow stronger: a calculus for differential privacy. In Proc. of ICFP, pages 157-168. ACM, 2010. Google Scholar
  31. Kimmo I. Rosenthal. Quantales and their applications / Kimmo I. Rosenthal. Pitman research notes in mathematics series ; 234. Longman Scientific & Technical, Essex, England, 1990. Google Scholar
  32. Davide Sangiorgi. A theory of bisimulation for the pi-calculus. In Proc. of CONCUR, volume 715 of Lecture Notes in Computer Science, pages 127-142. Springer, 1993. Google Scholar
  33. Franck van Breugel, Claudio Hermida, Michael Makkai, and James Worrell. An accessible approach to behavioural pseudometrics. In Proc. of ICALP, volume 3580 of LNCS, pages 1018-1030. Springer, 2005. Google Scholar
  34. Franck van Breugel and James Worrell. Approximating and computing behavioural distances in probabilistic transition systems. Theor. Comput. Sci., 360(1-3):373-385, 2006. Google Scholar
  35. Rob J. van Glabbeek. Notes on the methodology of CCS and CSP. Theor. Comput. Sci., 177(2):329-349, 1997. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact