Document Open Access Logo

Effectful Mealy Machines: Coalgebraic and Causal Traces (Invited Talk)

Authors Filippo Bonchi , Elena Di Lavore , Mario Román

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CALCO.2025.1.pdf
  • Filesize: 1.05 MB
  • 7 pages
HTML5 Logo HTML (experimental)
LIPIcs.CALCO.2025.1.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Abstract machines
Keywords
  • Mealy machines
  • coinduction
  • copy-discard categories
  • premonoidal categories

Metrics

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

Abstract

We introduce effectful Mealy machines - a general notion of Mealy machine with global effects - and give them semantics in terms of both bisimilarity and traces. Bisimilarity of effectful Mealy machines is characterized syntactically, via free uniform feedback. Their traces are given a novel semantic coinductive universe in terms of effectful streams. We prove that this framework generalizes standard causal processes and captures existing flavours of Mealy machine, bisimilarity, and trace.
This is an extended abstract for the manuscript Effectful Mealy Machines: Bisimulation and Trace that will appear in the proceedings of LiCS 2025 [Bonchi et al., 2025]; an extended version with proofs is also available (arxiv.org/abs/2410.10627) [Bonchi et al., 2025]. We additionally characterise causal processes as lax-natural transformations.

Cite As Get BibTex

Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful Mealy Machines: Coalgebraic and Causal Traces (Invited Talk). In 11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 342, pp. 1:1-1:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CALCO.2025.1

Author Details

Filippo Bonchi
  • Universitá di Pisa, Italy
Elena Di Lavore
  • University of Oxford, UK
Mario Román
  • University of Oxford, UK

Funding

  • Bonchi, Filippo: supported by the the Italian Ministero dell'Università e della Ricerca, grant PRIN 2022, PNRR No. P2022HXNSC - RAP (Resource Awareness in Programming) and partially by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme. This study was carried out within the National Centre on HPC, Big Data and Quantum Computing - SPOKE 10 (Quantum Computing) and received funding from the European Union Next-GenerationEU - National Recovery and Resilience Plan (NRRP) – MISSION 4 COMPONENT 2, INVESTMENT N. 1.4 – CUP N. I53C22000690001.
  • Di Lavore, Elena: supported by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme.
  • Román, Mario: partially supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0038 and by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme.

References

  1. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  2. Richard Blute, Josée Desharnais, Abbas Edalat, and Prakash Panangaden. Bisimulation for labelled Markov processes. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 149-158, 1997. URL: https://doi.org/10.1109/LICS.1997.614943.
  3. Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful Mealy machines: bisimulation and trace. In Proceedings of the 40th Annual ACM/IEEE Symposium on Logic in Computer Science (to appear), 2025. Google Scholar
  4. Filippo Bonchi, Elena Di Lavore, and Mario Román. Effectful Mealy machines: bisimulation and trace (extended version), 2025. URL: https://arxiv.org/abs/2410.10627.
  5. Lorenzo Ceragioli, Elena Di Lavore, Giuseppe Lomurno, and Gabriele Tedeschi. A coalgebraic model of quantum bisimulation, 2024. to appear in the preceedings of Applied Category Theory 2024. Google Scholar
  6. Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Quantum bisimilarity via barbs and contexts: Curbing the power of non-deterministic observers. Proceedings of the ACM on Programming Languages, 8(POPL):1269-1297, 2023. URL: https://doi.org/10.1145/3632885.
  7. Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, and Gabriele Tedeschi. Effect semantics for quantum process calculi, 2024. to appear in the preceedings of CONCUR 2024. Google Scholar
  8. Kenta Cho and Bart Jacobs. Disintegration and bayesian inversion via string diagrams. Mathematical Structures in Computer Science, 29(7):938-971, 2019. URL: https://doi.org/10.1017/S0960129518000488.
  9. Elena Di Lavore, Giovanni de Felice, and Mario Román. Monoidal streams for dataflow programming. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3531130.3533365.
  10. Elena Di Lavore and Mario Román. Evidential decision theory via partial Markov categories. In 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-14, 2023. URL: https://doi.org/10.1109/LICS56636.2023.10175776.
  11. Elena Di Lavore, Mario Román, Paweł Sobociński, and Márk Széles. Order in partial Markov categories. In Proceedings of the 41st Conference on Mathematical Foundations of Programming Semantics (to appear), 2025. Google Scholar
  12. Tobias Fritz. A synthetic approach to Markov kernels, conditional independence and theorems on sufficient statistics. Advances in Mathematics, 370:107239, 2020. Google Scholar
  13. Alan Jeffrey. Premonoidal categories and a graphical view of programs, 1997. Google Scholar
  14. Piergiulio Katis, Nicoletta Sabadini, and Robert F. C. Walters. Bicategories of processes. Journal of Pure and Applied Algebra, 115(2):141-178, 1997. URL: https://doi.org/10.1016/S0022-4049(96)00012-6.
  15. Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11-13, 1989, pages 344-352. ACM Press, 1989. URL: https://doi.org/10.1145/75277.75307.
  16. John Power and Edmund Robinson. Premonoidal categories and notions of computation. Math. Struct. Comput. Sci., 7(5):453-468, 1997. URL: https://doi.org/10.1017/S0960129597002375.
  17. George N Raney. Sequential functions. Journal of the ACM (JACM), 5(2):177-180, 1958. URL: https://doi.org/10.1145/320924.320930.
  18. Jan Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249(1):3-80, 2000. Modern Algebra. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  19. Sam Staton. Relating coalgebraic notions of bisimulation. In Alexander Kurz, Marina Lenisa, and Andrzej Tarlecki, editors, Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009, Udine, Italy, September 7-10, 2009. Proceedings, volume 5728 of Lecture Notes in Computer Science, pages 191-205. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03741-2_14.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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