Document Open Access Logo

A Complete Inference System for Probabilistic Infinite Trace Equivalence

Authors Corina Cîrstea , Lawrence S. Moss , Victoria Noquez , Todd Schmid , Alexandra Silva , Ana Sokolova

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2025.30.pdf
  • Filesize: 0.88 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Theory of computation → Formal languages and automata theory
Keywords
  • Coalgebra
  • infinite trace
  • semantics
  • logic
  • convex sets

Metrics

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

Abstract

We present the first sound and complete axiomatization of infinite trace semantics for generative probabilistic transition systems. Our approach is categorical, and we build on recent results on proper functors over convex sets. At the core of our proof is a characterization of infinite traces as the final coalgebra of a functor over convex algebras. Somewhat surprisingly, our axiomatization of infinite trace semantics coincides with that of finite trace semantics, even though the techniques used in the completeness proof are significantly different.

Cite As Get BibTex

Corina Cîrstea, Lawrence S. Moss, Victoria Noquez, Todd Schmid, Alexandra Silva, and Ana Sokolova. A Complete Inference System for Probabilistic Infinite Trace Equivalence. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 30:1-30:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.30

Author Details

Corina Cîrstea
  • University of Southampton, UK
Lawrence S. Moss
  • Indiana University, Bloomington, IN, USA
Victoria Noquez
  • Saint Mary’s College of California, Moraga, CA, USA
Todd Schmid
  • Bucknell University, Lewisburg, PA, USA
Alexandra Silva
  • Cornell University, Ithaca, NY, USA
Ana Sokolova
  • Paris Lodron University of Salzburg, Austria

Funding

This material is based upon work supported by the National Science Foundation under Grant No. DMS-1928930, while the authors were in residence at the Mathematical Sciences Research Institute in Berkeley, California, during the Summer Research in Mathematics program of 2024.
  • Cîrstea, Corina: partly supported by the Leverhulme Trust Research Project Grant RPG-2020-232.
  • Moss, Lawrence S.: Lawrence S. Moss was supported by grant #586136 from the Simons Foundation.
  • Silva, Alexandra: ERC grant Autoprobe (no. 101002697). This work was done in part while the author was visiting the Simons Institute for the Theory of Computing.

Acknowledgements

We thank Wojtek Rozowski for insightful discussions on related topics and the anonymous reviewers for helpful suggestions that improved the material presented in the paper. We thank the National Science Foundation and the Simons Laufer Mathematical Sciences Institute for their support of our work.

References

  1. J. Adámek and J. Rosicky. Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. Google Scholar
  2. M. Barr and Ch. Wells. Toposes, Triples and Theories. Springer, Berlin, 1985. Revised and corrected version available from URL: www.cwru.edu/artsci/math/wells/pub/ttt.html.
  3. F. Bartels, A. Sokolova, and E.P. de Vink. A hierarchy of probabilistic system types. Theoretical Computer Science, 327:3-22, 2004. URL: https://doi.org/10.1016/J.TCS.2004.07.019.
  4. Corina Cîrstea. From branching to linear time, coalgebraically. Fundam. Informaticae, 150(3-4):379-406, 2017. URL: https://doi.org/10.3233/FI-2017-1474.
  5. Alexandre Goy. Trace semantics via determinization for probabilistic transition systems. CoRR, abs/1802.09084, 2018. URL: https://arxiv.org/abs/1802.09084.
  6. Alexandre Goy and Jurriaan Rot. (In)finite trace equivalence of probabilistic transition systems. In Corina Cîrstea, editor, Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, volume 11202 of Lecture Notes in Computer Science, pages 100-121. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-00389-0_7.
  7. Antonius J. C. Hurkens, Monica McArthur, Yiannis N. Moschovakis, Lawrence S. Moss, and Glen T. Whitney. The logic of recursive equations. J. Symb. Log., 63(2):451-478, 1998. URL: https://doi.org/10.2307/2586843.
  8. Bart Jacobs. A bialgebraic review of deterministic automata, regular expressions and languages. In Kokichi Futatsugi, Jean-Pierre Jouannaud, and José Meseguer, editors, Algebra, Meaning, and Computation, Essays Dedicated to Joseph A. Goguen on the Occasion of His 65th Birthday, volume 4060 of Lecture Notes in Computer Science, pages 375-404. Springer, 2006. URL: https://doi.org/10.1007/11780274_20.
  9. Henning Kerstan and Barbara König. Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems. Logical Methods in Computer Science, Volume 9, Issue 4, December 2013. URL: https://doi.org/10.2168/LMCS-9(4:16)2013.
  10. S. C. Kleene. Representation of events in nerve nets and finite automata. In Claude Shannon and John McCarthy, editors, Automata Studies, pages 3-41. Princeton University Press, Princeton, NJ, 1956. Google Scholar
  11. Kim Guldstrand Larsen and Arne Skou. Bisimulation through probabilistic testing. Inf. Comput., 94(1):1-28, 1991. URL: https://doi.org/10.1016/0890-5401(91)90030-6.
  12. Radu Mardare, Prakash Panangaden, and Gordon Plotkin. Quantitative algebraic reasoning. In 2016 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-10, 2016. Google Scholar
  13. Stefan Milius. A sound and complete calculus for finite stream circuits. In Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science, LICS 2010, pages 421-430. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/LICS.2010.11.
  14. Stefan Milius. Proper functors and fixed points for finite behaviour. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:22)2018.
  15. Robin Milner. A complete inference system for a class of regular behaviours. J. Comput. Syst. Sci., 28(3):439-466, 1984. URL: https://doi.org/10.1016/0022-0000(84)90023-0.
  16. Michael O. Rabin. Probabilistic automata. Inf. Control., 6(3):230-245, 1963. URL: https://doi.org/10.1016/S0019-9958(63)90290-0.
  17. Alexander Moshe Rabinovich. A complete axiomatisation for trace congruence of finite state behaviors. In Stephen D. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, Mathematical Foundations of Programming Semantics, 9th International Conference, New Orleans, LA, USA, April 7-10, 1993, Proceedings, volume 802 of Lecture Notes in Computer Science, pages 530-543. Springer, 1993. URL: https://doi.org/10.1007/3-540-58027-1_25.
  18. Wojciech Rozowski and Alexandra Silva. A completeness theorem for probabilistic regular expressions. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 66:1-66:14. ACM, 2024. URL: https://doi.org/10.1145/3661814.3662084.
  19. Walter Rudin. Real and Complex Analysis. McGraw-Hill, 1966. Google Scholar
  20. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  21. Todd Schmid, Victoria Noquez, and Lawrence S. Moss. Fractals from regular behaviours. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science, CALCO 2023, June 19-21, 2023, Indiana University Bloomington, IN, USA, volume 270 of LIPIcs, pages 14:1-14:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Also available at https://arxiv.org/pdf/2306.03894. URL: https://doi.org/10.4230/LIPICS.CALCO.2023.14.
  22. Todd Schmid, Jurriaan Rot, and Alexandra Silva. On star expressions and coalgebraic completeness theorems. In Ana Sokolova, editor, Proceedings 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, Hybrid: Salzburg, Austria and Online, 30th August - 2nd September, 2021, volume 351 of EPTCS, pages 242-259, 2021. URL: https://doi.org/10.4204/EPTCS.351.15.
  23. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci., 9(1), 2013. URL: https://doi.org/10.2168/LMCS-9(1:9)2013.
  24. Alexandra Silva, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Non-deterministic kleene coalgebras. Log. Methods Comput. Sci., 6(3), 2010. URL: http://arxiv.org/abs/1007.3769.
  25. Alexandra Silva and Ana Sokolova. Sound and complete axiomatization of trace semantics for probabilistic systems. In Michael W. Mislove and Joël Ouaknine, editors, Twenty-seventh Conference on the Mathematical Foundations of Programming Semantics, MFPS 2011, Pittsburgh, PA, USA, May 25-28, 2011, volume 276 of Electronic Notes in Theoretical Computer Science, pages 291-311. Elsevier, 2011. URL: https://doi.org/10.1016/j.entcs.2011.09.027.
  26. A. Sokolova and E.P. de Vink. Probabilistic automata: system types, parallel composition and comparison. In C. Baier, B.R. Haverkort, H. Hermanns, J.-P. Katoen, and M. Siegle, editors, Validation of Stochastic Systems: A Guide to Current Research, pages 1-43. LNCS 2925, 2004. URL: https://doi.org/10.1007/978-3-540-24611-4_1.
  27. Ana Sokolova and Harald Woracek. Congruences of convex algebras. Journal of Pure and Applied Algebra, 219(8):3110-3148, 2015. URL: https://doi.org/10.1016/j.jpaa.2014.10.005.
  28. Ana Sokolova and Harald Woracek. Proper semirings and proper convex functors. In FoSSaCS 2018, pages 331-347. LNCS 10803, 2018. Google Scholar
  29. Eugene W. Stark and Scott A. Smolka. A complete axiom system for finite-state probabilistic processes. In Gordon D. Plotkin, Colin Stirling, and Mads Tofte, editors, Proof, Language, and Interaction, Essays in Honour of Robin Milner, pages 571-596. The MIT Press, 2000. Google Scholar
  30. Sam Staton. Relating coalgebraic notions of bisimulation. In CALCO 2009, volume 5728, pages 191-205. LNCS 5728, 2009. URL: https://doi.org/10.1007/978-3-642-03741-2_14.
  31. T. Świrszcz. Monadic functors and convexity. Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 22:39-42, 1974. Google Scholar
  32. Natsuki Urabe and Ichiro Hasuo. Coalgebraic infinite traces and Kleisli simulations. Log. Methods Comput. Sci., 14(3), 2018. URL: https://doi.org/10.23638/LMCS-14(3:15)2018.
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