Document Open Access Logo

Up-To Techniques for Behavioural Metrics via Fibrations

Authors Filippo Bonchi, Barbara König, Daniela Petrisan

PDF

File

Thumbnail PDF
PDF
LIPIcs.CONCUR.2018.17.pdf
  • Filesize: 0.52 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Formal languages and automata theory
  • Theory of computation → Logic and verification
Keywords
  • behavioural metrics
  • bisimilarity
  • up-to techniques
  • coalgebras
  • fibrations

Metrics

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

Abstract

Up-to techniques are a well-known method for enhancing coinductive proofs of behavioural equivalences. We introduce up-to techniques for behavioural metrics between systems modelled as coalgebras and we provide abstract results to prove their soundness in a compositional way.
In order to obtain a general framework, we need a systematic way to lift functors: we show that the Wasserstein lifting of a functor, introduced in a previous work, corresponds to a change of base in a fibrational sense. This observation enables us to reuse existing results about soundness of up-to techniques in a fibrational setting. We focus on the fibrations of predicates and relations valued in a quantale, for which pseudo-metric spaces are an example. To illustrate our approach we provide an example on distances between regular languages.

Cite As Get BibTex

Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-To Techniques for Behavioural Metrics via Fibrations. In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018) https://doi.org/10.4230/LIPIcs.CONCUR.2018.17

Author Details

Filippo Bonchi
  • Universitá di Pisa, Italy
Barbara König
  • Universität Duisburg-Essen, Germany
Daniela Petrisan
  • CNRS, IRIF, Université Paris Diderot, France

Funding

The first author acknowledges financial support from project ANR-16-CE25-0011 REPAS, the second author from DFG project BEMEGA, and the third author from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No.670624).

References

  1. G. Bacci, G. Bacci, K.G. Larsen, and R. Mardare. Computing behavioral distances, compositionally. In Proc. of MFCS '13, pages 74-85. Springer, 2013. LNCS 8087. Google Scholar
  2. A. Balan, A. Kurz, and J. Velebil. Extensions of functors from Set to 𝒱-cat. In CALCO, volume 35 of LIPIcs, pages 17-34, 2015. Google Scholar
  3. P. Baldan, F. Bonchi, H. Kerstan, and B. König. Behavioral metrics via functor lifting. In FSTTCS, volume 29 of LIPIcs, 2014. Google Scholar
  4. P. Baldan, F. Bonchi, H. Kerstan, and B. König. Towards trace metrics via functor lifting. In CALCO, volume 35 of LIPIcs, pages 35-49, 2015. Google Scholar
  5. P. Baldan, F. Bonchi, H. Kerstan, and B. König. Coalgebraic behavioral metrics. LMCS, to appear. arXiv:1712.07511. Google Scholar
  6. F. Bonchi, P. Ganty, R. Giacobazzi, and D. Pavlovic. Sound up-to techniques and complete abstract domains. In Proc. of LICS '18, 2018. Google Scholar
  7. F. Bonchi, B. König, and S. Küpper. Up-to techniques for weighted systems. In Proc. of TACAS '17, Part I, pages 535-552. Springer, 2017. LNCS 10205. Google Scholar
  8. F. Bonchi, B. König, and D. Petrişan. Up-to techniques for behavioural metrics via fibrations, 2018. arXiv:1806.11064. URL: http://arxiv.org/abs/1806.11064.
  9. F. Bonchi, D. Petrişan, D. Pous, and J. Rot. Coinduction up-to in a fibrational setting. In CSL-LICS. ACM, 2014. Paper No. 20. Google Scholar
  10. F. Bonchi and D. Pous. Checking NFA equivalence with bisimulations up to congruence. In POPL, pages 457-468. ACM, 2013. Google Scholar
  11. K. Chatzikokolakis, D. Gebler, C. Palamidessi, and L. Xu. Generalized bisimulation metrics. In Proc. of CONCUR '14. Springer, 2014. LNCS/ARCoSS 8704. Google Scholar
  12. K. Chatzikokolakis, C. Palamidessi, and V. Vignudelli. Up-to techniques for generalized bisimulation metrics. In CONCUR, volume 59 of LIPIcs, pages 35:1-35:14, 2016. Google Scholar
  13. N.A. Danielsson. Up-to techniques using sized types. Proc. ACM Program. Lang., 2(POPL):43:1-43:28, 2017. Google Scholar
  14. L. de Alfaro, M. Faella, and M. Stoelinga. Linear and branching metrics for quantitative transition systems. In ICALP, pages 97-109. Springer, 2004. LNCS 3142. Google Scholar
  15. J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labelled Markov processes. Theor. Comput. Sci., 318(3):323-354, 2004. Google Scholar
  16. M. Droste, W. Kuich, and H. Vogler. Handbook of Weighted Automata. Monographs in Theoretical Computer Science. Springer, 2009. Google Scholar
  17. I. Hasuo. Generic weakest precondition semantics from monads enriched with order. Theor. Comput. Sci., 604:2-29, 2015. Google Scholar
  18. C. Hermida and B. Jacobs. Structural induction and coinduction in a fibrational setting. Inf. and Comp., 145:107-152, 1998. Google Scholar
  19. D. Hofmann. Topological theories and closed objects. Advances in Mathematics, 215(2):789-824, 2007. Google Scholar
  20. C.-K. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. The power of parameterization in coinductive proof. In POPL, pages 193-206. ACM, 2013. Google Scholar
  21. B. Jacobs. Categorical Logic and Type Theory. Elsevier, 1999. Google Scholar
  22. B. Jacobs. Introduction to coalgebra. Towards mathematics of states and observations. Cambridge University Press, 2016. Google Scholar
  23. B. Jacobs, A. Silva, and A. Sokolova. Trace semantics via determinization. J. Comput. Syst. Sci., 81(5):859-879, 2015. URL: http://dx.doi.org/10.1016/j.jcss.2014.12.005.
  24. S. Katsumata and T. Sato. Codensity liftings of monads. In CALCO, volume 35 of LIPIcs, pages 156-170, 2015. Google Scholar
  25. M. Kelly. Basic Concepts of Enriched Category Theory, volume 64 of Lecture Notes in Mathematics. Cambridge University Press, 1982. Google Scholar
  26. B. Klin. Bialgebras for structural operational semantics: An introduction. Theor. Comput. Sci., 412(38):5043-5069, 2011. URL: http://dx.doi.org/10.1016/j.tcs.2011.03.023.
  27. F.W. Lawvere. Metric spaces, generalized logic, and closed categories. Reprints in Theory and Applications of Categories, pages 1-37, 2002. Google Scholar
  28. R. Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  29. R. Milner and D. Sangiorgi. Techniques of weak bisimulation up-to. In CONCUR. Springer-Verlag, 1992. LNCS 630. Google Scholar
  30. J. Parrow and T. Weber. The largest respectful function, 2016. arXiv:1605.04136. Google Scholar
  31. D. Pous. Complete lattices and up-to techniques. In APLAS, volume 4807 of LNCS, pages 351-366. Springer, 2007. Google Scholar
  32. D. Pous. Coinduction all the way up. In Proc. of LICS '16, pages 307-316. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2934564.
  33. D. Pous and D. Sangiorgi. Enhancements of the coinductive proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2011. Google Scholar
  34. J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical computer science, 249(1):3-80, 2000. Google Scholar
  35. D. Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science, 8(5):447-479, 1998. Google Scholar
  36. L. Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comp. Sci., 390:230-247, 2008. Google Scholar
  37. A. Silva, F. Bonchi, M. M. Bonsangue, and J.J.M.M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1), 2013. URL: http://dx.doi.org/10.2168/LMCS-9(1:9)2013.
  38. S. Tini, K.G. Larsen, and D. Gebler. Compositional bisimulation metric reasoning with probabilistic process calculi. Logical Methods in Computer Science, 12, 2017. Google Scholar
  39. D. Turi and G. Plotkin. Towards a mathematical operational semantics. In Proc. of LICS '97, pages 280-291. IEEE, 1997. Google Scholar
  40. F. van Breugel and J. Worrell. Towards quantitative verification of probabilistic transition systems. In ICALP, volume 2076 of LNCS, pages 421-432. Springer, 2001. Google Scholar
  41. F. van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems. Theor. Comp. Sci., 331:115-142, 2005. Google Scholar
  42. C. Villani. Optimal Transport - Old and New, volume 338 of A Series of Comprehensive Studies in Mathematics. Springer, 2009. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact