Document Open Access Logo

Processes Parametrised by an Algebraic Theory

Authors Todd Schmid , Wojciech Różowski , Jurriaan Rot, Alexandra Silva

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2022.132.pdf
  • Filesize: 0.92 MB
  • 20 pages

Document Identifiers

Author Details

Todd Schmid
  • Department of Computer Science, University College London, UK
Wojciech Różowski
  • Department of Computer Science, University College London, UK
Jurriaan Rot
  • Institute for Computing and Information Sciences, Radboud University, Nijmegen, The Netherlands
Alexandra Silva
  • Department of Computer Science, Cornell University, Ithaca, NY, USA

Funding

  • Schmid, Todd: Partially supported by ERC grant Autoprobe (grant agreement 101002697).
  • Różowski, Wojciech: Partially supported by ERC grant Autoprobe (grant agreement 101002697).
  • Silva, Alexandra: Partially supported by ERC grant Autoprobe (grant agreement 101002697) and a Royal society Wolfson fellowship.

Cite As Get BibTex

Todd Schmid, Wojciech Różowski, Jurriaan Rot, and Alexandra Silva. Processes Parametrised by an Algebraic Theory. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 132:1-132:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ICALP.2022.132

Abstract

We develop a (co)algebraic framework to study a family of process calculi with monadic branching structures and recursion operators. Our framework features a uniform semantics of process terms and a complete axiomatisation of semantic equivalence. We show that there are uniformly defined fragments of our calculi that capture well-known examples from the literature like regular expressions modulo bisimilarity and guarded Kleene algebra with tests. We also derive new calculi for probabilistic and convex processes with an analogue of Kleene star.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program reasoning
Keywords
  • process algebra
  • program semantics
  • coalgebra
  • regular expressions

Metrics

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

Related Versions

References

  1. Suzana Andova. Process algebra with probabilistic choice. In Joost-Pieter Katoen, editor, Formal Methods for Real-Time and Probabilistic Systems, 5th International AMAST Workshop, ARTS'99, Bamberg, Germany, May 26-28, 1999. Proceedings, volume 1601 of Lecture Notes in Computer Science, pages 111-129. Springer, 1999. URL: https://doi.org/10.1007/3-540-48778-6_7.
  2. Jos C. M. Baeten. A brief history of process algebra. Theor. Comput. Sci., 335(2-3):131-146, 2005. URL: https://doi.org/10.1016/j.tcs.2004.07.036.
  3. Jos C. M. Baeten, Flavio Corradini, and Clemens Grabmayer. On the star height of regular expressions under bisimulation (extended abstract), 2006. Google Scholar
  4. Michael Barr. Terminal coalgebras in well-founded set theory. Theor. Comput. Sci., 114(2):299-315, 1993. URL: https://doi.org/10.1016/0304-3975(93)90076-6.
  5. Jan A. Bergstra and Jan Willem Klop. Process theory based on bisimulation semantics. In J. W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, editors, Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, School/Workshop, Noordwijkerhout, The Netherlands, May 30 - June 3, 1988, Proceedings, volume 354 of Lecture Notes in Computer Science, pages 50-122. Springer, 1988. URL: https://doi.org/10.1007/BFb0013021.
  6. Stephen L. Bloom and Calvin C. Elgot. The existence and construction of free iterative theories. J. Comput. Syst. Sci., 12(3):305-318, 1976. URL: https://doi.org/10.1016/S0022-0000(76)80003-7.
  7. Stephen L. Bloom and Zoltán Ésik. Varieties of iteration theories. SIAM J. Comput., 17(5):939-966, 1988. URL: https://doi.org/10.1137/0217059.
  8. Stephen L. Bloom and Ralph Tindell. Varieties of "if-then-else". SIAM J. Comput., 12(4):677-707, 1983. URL: https://doi.org/10.1137/0212047.
  9. Filippo Bonchi and Alessio Santamaria. Combining semilattices and semimodules. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures - 24th International Conference, FOSSACS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, volume 12650 of Lecture Notes in Computer Science, pages 102-123. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71995-1_6.
  10. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The power of convex algebras. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.23.
  11. Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism and probability. In 34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019, pages 1-14. IEEE, 2019. URL: https://doi.org/10.1109/LICS.2019.8785673.
  12. Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases. In Fabio Gadducci and Alexandra Silva, editors, 9th Conference on Algebra and Coalgebra in Computer Science (CALCO 2021), volume 211 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1-11:18, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CALCO.2021.11.
  13. Calvin C. Elgot. Monadic computation and iterative algebraic theories. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 175-230. Elsevier, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71949-9.
  14. Wan Fokkink. Axiomatizations for the perpetual loop in process algebra. In Pierpaolo Degano, Roberto Gorrieri, and Alberto Marchetti-Spaccamela, editors, Automata, Languages and Programming, pages 571-581, Berlin, Heidelberg, 1997. Springer Berlin Heidelberg. Google Scholar
  15. Wan J. Fokkink and Hans Zantema. Basic process algebra with iteration: Completeness of its equational axioms. Comput. J., 37(4):259-268, 1994. URL: https://doi.org/10.1093/comjnl/37.4.259.
  16. Wan J. Fokkink and Hans Zantema. Termination modulo equations by abstract commutation with an application to iteration. Theor. Comput. Sci., 177(2):407-423, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00254-X.
  17. Nate Foster, Dexter Kozen, Konstantinos Mamouras, Mark Reitblatt, and Alexandra Silva. Probabilistic netkat. In Peter Thiemann, editor, Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9632 of Lecture Notes in Computer Science, pages 282-309. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_12.
  18. Joseph A. Goguen, James W. Thatcher, Eric G. Wagner, and Jesse B. Wright. Initial algebra semantics and continuous algebras. J. ACM, 24(1):68-95, 1977. URL: https://doi.org/10.1145/321992.321997.
  19. Clemens Grabmayer. A coinductive version of milner’s proof system for regular expressions modulo bisimilarity. In Fabio Gadducci and Alexandra Silva, editors, 9th Conference on Algebra and Coalgebra in Computer Science, CALCO 2021, August 31 to September 3, 2021, Salzburg, Austria, volume 211 of LIPIcs, pages 16:1-16:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CALCO.2021.16.
  20. Clemens Grabmayer and Wan J. Fokkink. A complete proof system for 1-free regular expressions modulo bisimilarity. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, pages 465-478. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394744.
  21. H. Peter Gumm. Elements of the general theory of coalgebras. LUATCS'99, Rand Afrikaans University, Johannesburg, 1999. Google Scholar
  22. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Methods Comput. Sci., 3(4), 2007. URL: https://doi.org/10.2168/LMCS-3(4:11)2007.
  23. Bart Jacobs. Convexity, duality and effects. In Cristian S. Calude and Vladimiro Sassone, editors, Theoretical Computer Science - 6th IFIP TC 1/WG 2.2 International Conference, TCS 2010, Held as Part of WCC 2010, Brisbane, Australia, September 20-23, 2010. Proceedings, volume 323 of IFIP Advances in Information and Communication Technology, pages 1-19. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-15240-5_1.
  24. Dexter Kozen and Wei-Lung Dustin Tseng. The böhm-jacopini theorem is false, propositionally. In Philippe Audebaud and Christine Paulin-Mohring, editors, Mathematics of Program Construction, 9th International Conference, MPC 2008, Marseille, France, July 15-18, 2008. Proceedings, volume 5133 of Lecture Notes in Computer Science, pages 177-192. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-70594-9_11.
  25. Joachim Lambek. A fixpoint theorem for complete categories. Mathematische Zeitschrift, 103(2):151-161, 1968. Google Scholar
  26. Ernest G. Manes. Algebraic Theories. Graduate Texts in Mathematics. Springer-Verlag New York, 1 edition, 1976. URL: https://doi.org/10.1007/978-1-4612-9860-1.
  27. Ernest G. Manes. Equations for if-then-else. In Stephen D. Brookes, Michael G. Main, Austin Melton, Michael W. Mislove, and David A. Schmidt, editors, Mathematical Foundations of Programming Semantics, 7th International Conference, Pittsburgh, PA, USA, March 25-28, 1991, Proceedings, volume 598 of Lecture Notes in Computer Science, pages 446-456. Springer, 1991. URL: https://doi.org/10.1007/3-540-55511-0_23.
  28. John McCarthy. A basis for a mathematical theory of computation, preliminary report. In Walter F. Bauer, editor, Papers presented at the 1961 western joint IRE-AIEE-ACM computer conference, IRE-AIEE-ACM 1961 (Western), Los Angeles, California, USA, May 9-11, 1961, pages 225-238. ACM, 1961. URL: https://doi.org/10.1145/1460690.1460715.
  29. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  30. 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.
  31. Michael W. Mislove, Joël Ouaknine, and James Worrell. Axioms for probability and nondeterminism. In Flavio Corradini and Uwe Nestmann, editors, Proceedings of the 10th International Workshop on Expressiveness in Concurrency, EXPRESS 2003, Marseille, France, September 2, 2003, volume 96 of Electronic Notes in Theoretical Computer Science, pages 7-28. Elsevier, 2003. URL: https://doi.org/10.1016/j.entcs.2004.04.019.
  32. Robert S. R. Myers. Coalgebraic expressions. In Ralph Matthes and Tarmo Uustalu, editors, 6th Workshop on Fixed Points in Computer Science, FICS 2009, Coimbra, Portugal, September 12-13, 2009, pages 61-69. Institute of Cybernetics, 2009. URL: http://cs.ioc.ee/fics09/proceedings/contrib8.pdf.
  33. Evelyn Nelson. Iterative algebras. Theor. Comput. Sci., 25:67-94, 1983. URL: https://doi.org/10.1016/0304-3975(83)90014-2.
  34. Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebraic Methods Program., 60-61:17-139, 2004. Google Scholar
  35. D. Pumplün and Helmut Röhrl. Convexity theories IV. klein-hilbert parts in convex modules. Appl. Categorical Struct., 3(2):173-200, 1995. URL: https://doi.org/10.1007/BF00877635.
  36. Jan J. M. M. Rutten. Automata and coinduction (an exercise in coalgebra). In Davide Sangiorgi and Robert de Simone, editors, CONCUR '98: Concurrency Theory, 9th International Conference, Nice, France, September 8-11, 1998, Proceedings, volume 1466 of Lecture Notes in Computer Science, pages 194-218. Springer, 1998. URL: https://doi.org/10.1007/BFb0055624.
  37. 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.
  38. Jan J. M. M. Rutten and Daniele Turi. On the foundations of final semantics: Non-standard sets, metric spaces, partial orders. In J. W. de Bakker, W. P. de Roever, and G. Rozenberg, editors, Semantics: Foundations and Applications, pages 477-530, Berlin, Heidelberg, 1993. Springer Berlin Heidelberg. Google Scholar
  39. Arto Salomaa. Two complete axiom systems for the algebra of regular events. J. ACM, 13(1):158-169, 1966. URL: https://doi.org/10.1145/321312.321326.
  40. Todd Schmid, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded kleene algebra with tests: Coequations, coinduction, and completeness. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs, pages 142:1-142:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ICALP.2021.142.
  41. 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.
  42. Todd Schmid, Wojciech Rozowski, Alexandra Silva, and Jurriaan Rot. Processes parametrised by an algebraic theory (with appendix), 2022. URL: http://arxiv.org/abs/2202.06901.
  43. Alexandra Silva. Kleene coalgebra. PhD thesis, University of Nijmegen, 2010. Google Scholar
  44. Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva. Guarded kleene algebra with tests: verification of uninterpreted programs in nearly linear time. Proc. ACM Program. Lang., 4(POPL):61:1-61:28, 2020. URL: https://doi.org/10.1145/3371129.
  45. 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
  46. Marshall Harvey Stone. Postulates for the barycentric calculus. Annali di Matematica Pura ed Applicata, 29(1):25-30, 1949. Google Scholar
  47. Tadeusz Świrszcz. Monadic functors and convexity. Bulletin de L'Académie Polonaise des Sciences, XXII(1):39-42, 1974. Google Scholar
  48. Daniele Turi and Gordon D. Plotkin. Towards a mathematical operational semantics. In Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29 - July 2, 1997, pages 280-291. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614955.
  49. Daniele Varacca and Glynn Winskel. Distributing probability over non-determinism. Mathematical Structures in Computer Science, 16(1):87-113, 2006. URL: https://doi.org/10.1017/S0960129505005074.
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