Document Open Access Logo

Towards Trace Metrics via Functor Lifting

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

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2015.35.pdf
  • Filesize: 0.55 MB
  • 15 pages

Document Identifiers

Author Details

Paolo Baldan
Filippo Bonchi
Henning Kerstan
Barbara König

Cite As Get BibTex

Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Towards Trace Metrics via Functor Lifting. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 35-49, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CALCO.2015.35

Abstract

We investigate the possibility of deriving metric trace semantics in a coalgebraic framework. First, we generalize a technique for systematically lifting functors from the category Set of sets to the category PMet of pseudometric spaces, by identifying conditions under which also natural transformations, monads and distributive laws can be lifted. By exploiting some recent work on an abstract determinization, these results enable the derivation of trace metrics starting from coalgebras in Set. More precisely, for a coalgebra in Set we determinize it, thus obtaining a coalgebra in the Eilenberg-Moore category of a monad. When the monad can be lifted to PMet, we can equip the final coalgebra with a behavioral distance. The trace distance between two states of the original coalgebra is the distance between their images in the determinized coalgebra through the unit of the monad. We show how our framework applies to nondeterministic automata and probabilistic automata.

Subject Classification

Keywords
  • trace metric
  • monad lifting
  • pseudometric
  • coalgebra

Metrics

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

References

  1. Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, and Radu Mardare. On the total variation distance of semi-markov chains. In Foundations of Software Science and Computation Structures (FOSSACS 2015), volume 9034 of Lecture Notes in Computer Science. Springer, 2015. Google Scholar
  2. Paolo Baldan, Filippo Bonchi, Henning Kerstan, and Barbara König. Behavioral Metrics via Functor Lifting. In Venkatesh Raman and S. P. Suresh, editors, 34th International Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2014), volume 29 of Leibniz International Proceedings in Informatics (LIPIcs), pages 403-415. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2014. Google Scholar
  3. 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
  4. Konstantinos Chatzikokolakis, Daniel Gebler, Catuscia Palamidessi, and Lili Xu. Generalized bisimulation metrics. In CONCUR 2014 - Concurrency Theory, Lecture Notes in Computer Science, pages 32-46, 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'04, volume 3142 of Lecture Notes in Computer Science, pages 97-109. Springer, 2004. 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. Josée Desharnais, Vineet Gupta, Radha Jagadeesan, and Prakash Panangaden. Metrics for labelled Markov processes. Theoretical Computer Science, 318(3):323-354, 2004. Google Scholar
  8. Uli Fahrenberg, Axel Legay, and Claus Thrane. The quantitative linear-time-branching-time spectrum. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011), volume 13 of Leibniz International Proceedings in Informatics (LIPIcs), pages 103-114. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. Google Scholar
  9. Daniel Gebler and Simone Tini. Compositionality of approximate bisimulation for probabilistic systems. In Proc. of EXPRESS/SOS'13, pages 32-46, 2013. Google Scholar
  10. 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
  11. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3 (4:11):1-36, November 2007. Google Scholar
  12. Bart Jacobs. Introduction to coalgebra. Towards mathematics of states and observations, 2012. Draft. Google Scholar
  13. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Dirk Pattinson and Lutz Schröder, editors, Coalgebraic Methods in Computer Science, volume 7399 of Lecture Notes in Computer Science, pages 109-129. Springer Berlin Heidelberg, 2012. Google Scholar
  14. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. Journal of Computer and System Sciences, 81(5):859-879, 2015. 11th International Workshop on Coalgebraic Methods in Computer Science, CMCS 2012 (Selected Papers). Google Scholar
  15. Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science, 412(38):5043-5069, 2011. Google Scholar
  16. E.G. Manes and M.A. Arbib. Algebraic approaches to program semantics. Texts and Monographs in Computer Science, 1986. Google Scholar
  17. John Power and Daniele Turi. A coalgebraic foundation for linear time semantics. Electronic Notes in Theoretical Computer Science, 29:259-274, 1999. Google Scholar
  18. J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249:3-80, 2000. Google Scholar
  19. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2-3):230-247, 2008. Google Scholar
  20. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Logical Methods in Computer Science, 9(1), 2013. Google Scholar
  21. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In Proc. of LICS'97, pages 280-291, 1997. Google Scholar
  22. Franck van Breugel. The metric monad for probabilistic nondeterminism, April 2005. Google Scholar
  23. Franck van Breugel and James Worrell. A behavioural pseudometric for probabilistic transition systems. Theoretical Computer Science, 331:115-142, 2005. Google Scholar
  24. Franck van Breugel and James Worrell. Approximating and computing behavioural distances in probabilistic transition systems. Theoretical Computer Science, 360(1):373-385, 2006. Google Scholar
  25. 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 About DROPS Imprint Privacy Contact