Document Open Access Logo

Behavioral Metrics via Functor Lifting

Authors Paolo Baldan, Filippo Bonchi, Henning Kerstan, Barbara König

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2014.403.pdf
  • Filesize: 0.52 MB
  • 13 pages

Document Identifiers

Author Details

Paolo Baldan
Filippo Bonchi
Henning Kerstan
Barbara König

Cite AsGet BibTex

Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral Metrics via Functor Lifting. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 403-415, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/LIPIcs.FSTTCS.2014.403

Abstract

We study behavioral metrics in an abstract coalgebraic setting. Given a coalgebra alpha : X -> FX in Set, where the functor F specifies the branching type, we define a framework for deriving pseudometrics on X which measure the behavioral distance of states. A first crucial step is the lifting of the functor F on Set to a functor /F in the category PMet of pseudometric spaces. We present two different approaches which can be viewed as generalizations of the Kantorovich and Wasserstein pseudometrics for probability measures. We show that the pseudometrics provided by the two approaches coincide on several natural examples, but in general they differ. Then a final coalgebra for F in Set can be endowed with a behavioral distance resulting as the smallest solution of a fixed-point equation, yielding the final /F-coalgebra in PMet. The same technique, applied to an arbitrary coalgebra alpha : X -> FX in Set, provides the behavioral distance on X. Under some constraints we can prove that two states are at distance 0 if and only if they are behaviorally equivalent.
Keywords
  • behavioral metric
  • functor lifting
  • pseudometric
  • coalgebra

Metrics

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

References

  1. Jiří Adámek. Free algebras and automata realizations in the language of categories. Commentationes Mathematicae Universitatis Carolinae, 015(4):589-602, 1974. Google Scholar
  2. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On-the-fly exact computation of bisimilarity distances. In Proc. of TACAS'13, pages 1-15, 2013. Google Scholar
  3. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral metrics via functor lifting. Extended version with proofs, see http://arxiv.org/abs/1410.3385, 2014.
  4. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. Coinduction up to in a fibrational setting. In Proc. of CSL-LICS'14, 2014. Google Scholar
  5. Di Chen, Franck van Breugel, and James Worrell. On the complexity of computing probabilistic bisimilarity. In Proc. of FoSSaCS'12, volume 7213 of LNCS, pages 437-451, 2012. Google Scholar
  6. Luca de Alfaro, Marco Faella, and Mariëlle Stoelinga. Linear and branching system metrics. IEEE Transactions on Software Engineering, 25(2), 2009. Google Scholar
  7. Yuxin Deng, Tom Chothia, Catuscia Palamidessi, and Jun Pang. Metrics for action-labelled quantitative transition systems. ENTCS, 153(2):79-96, 2006. Google Scholar
  8. Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. Information and Computation, 179(2):163-193, 2002. Google Scholar
  9. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. TCS, 318(3):323-354, 2004. Google Scholar
  10. Joseé Desharnais, Radha Jagadeesan, Vineet Gupta, and Prakash Panangaden. The metric analogue of weak bisimulation for probabilistic processes. In Proc. of LICS'02, pages 413-422. IEEE, 2002. Google Scholar
  11. Daniel Gebler and Simone Tini. Compositionality of approximate bisimulation for probabilistic systems. In Proc. of EXPRESS/SOS'13, pages 32-46, 2013. Google Scholar
  12. Alessandro Giacalone, Chi-Chang Jou, and Scott A. Smolka. Algebraic reasoning for probabilistic concurrent systems. In Proc. IFIP TC2 Working Conference on Programming Concepts and Methods, pages 443-458. North-Holland, 1990. Google Scholar
  13. Ichiro Hasuo, Kenta Cho, Toshiki Kataoka, and Bart Jacobs. Coinductive predicates and final sequences in a fibration. ENTCS, 298:197-214, 2013. Google Scholar
  14. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. LMCS, 3 (4:11):1-36, November 2007. Google Scholar
  15. Bartek Klin. Bialgebras for structural operational semantics: An introduction. TCS, 412(38):5043-5069, 2011. Google Scholar
  16. Kim G. Larsen and Arne Skou. Bisimulation through probabilistic testing. In Proc. of POPL'89, pages 344-352, 1989. Google Scholar
  17. J. J. M. M. Rutten. Universal coalgebra: a theory of systems. TCS, 249:3-80, 2000. Google Scholar
  18. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. TCS, 390(2-3):230-247, 2008. Google Scholar
  19. Ana Sokolova. Probabilistic systems coalgebraically: A survey. TCS, 412(38):5095-5110, 2011. CMCS Tenth Anniversary Meeting. Google Scholar
  20. Franck van Breugel, Claudio Hermida, Michael Makkai, and James Worrell. Recursively defined metric spaces without contraction. TCS, 380(1-2):143-163, July 2007. Google Scholar
  21. Franck van Breugel, Babita Sharma, and James Worrell. Approximating a behavioural pseudometric without discount for probabilistic systems. LMCS, 4(2), 2008. Google Scholar
  22. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. TCS, 331:115-142, 2005. Google Scholar
  23. Franck van Breugel and James Worrell. Approximating and computing behavioural distances in probabilistic transition systems. TCS, 360(1):373-385, 2006. Google Scholar
  24. Cédric 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact