Document Open Access Logo

Enhanced Induction in Behavioural Relations (Invited Talk)

Author Davide Sangiorgi

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.4.pdf
  • Filesize: 425 kB
  • 6 pages

Document Identifiers

Author Details

Davide Sangiorgi
  • University of Bologna, Italy
  • INRIA, Sophia Antipolis, France

Cite AsGet BibTex

Davide Sangiorgi. Enhanced Induction in Behavioural Relations (Invited Talk). In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 4:1-4:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CSL.2023.4

Abstract

We outline an attempt at transporting the well-known theory of enhancements for the coinduction proof method, widely used on behavioural relations such as bisimilarity, onto the realms of inductive behaviour relations, i.e., relations defined from inductive observables, and discuss relevant literature.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program semantics
Keywords
  • coinduction
  • induction
  • semantics
  • behavioural relations

Metrics

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

Related Versions

References

  1. Jos C. M. Baeten, Jan A. Bergstra, and Jan Willem Klop. Ready-trace semantics for concrete process algebra with the priority operator. Comput. J., 30(6):498-506, 1987. Google Scholar
  2. F. Bartels. Generalised coinduction. Math. Struct. in Computer Science, 13(2):321-348, 2003. URL: https://doi.org/10.1017/S0960129502003900.
  3. F. Bartels. On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam, April 2004. Google Scholar
  4. Henning Basold, Damien Pous, and Jurriaan Rot. Monoidal company for accessible functors. In Proc. CALCO, volume 72 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CALCO.2017.5.
  5. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-to techniques for behavioural metrics via fibrations. In Sven Schewe and Lijun Zhang, editors, CONCUR'18,, volume 118 of LIPIcs, pages 17:1-17:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2018.17.
  6. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. A general account of coinduction up-to. Acta Inf., 54(2):127-190, 2017. URL: https://doi.org/10.1007/s00236-016-0271-4.
  7. Stephen D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. J. ACM, 31(3):560-599, 1984. URL: https://doi.org/10.1145/828.833.
  8. Stephen D. Brookes and A. W. Roscoe. An improved failures model for communicating processes. In Stephen D. Brookes, A. W. Roscoe, and Glynn Winskel, editors, Seminar on Concurrency, volume 197 of Lecture Notes in Computer Science, pages 281-305. Springer Verlag, 1984. Google Scholar
  9. R. De Nicola and R. Hennessy. Testing equivalences for processes. Theoretical Computer Science, 34:83-133, 1984. Google Scholar
  10. Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Divergence and unique solution of equations. Logical Methods in Computer Science, 15(3), 2019. URL: https://doi.org/10.23638/LMCS-15(3:12)2019.
  11. R.J. van Glabbeek. The linear time - branching time spectrum II (the semantics of sequential systems with silent moves). In E. Best, editor, Proc. CONCUR '93, volume 715. Springer Verlag, 1993. URL: https://doi.org/10.1007/3-540-57208-2_6.
  12. R.J. van Glabbeek. The linear time - branching time spectrum I. In A. Ponse J. Bergstra and S. Smolka, editors, Handbook of Process Algebra, pages 3-99. Elsevier, 2001. URL: https://doi.org/10.1016/b978-044482830-9/50019-9.
  13. M. Hennessy. Algebraic Theory of Processes. The MIT Press, Cambridge, Mass., 1988. Google Scholar
  14. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137-161, 1985. Google Scholar
  15. Bart Jacobs. Distributive laws for the coinductive solution of recursive equations. Information and Computation, 204(4):561-587, 2006. URL: https://doi.org/10.1016/j.ic.2005.03.006.
  16. Marina Lenisa. From set-theoretic coinduction to coalgebraic coinduction: some results, some problems. Electronical Notes in Computer Science, 19:2-22, 1999. URL: https://doi.org/10.1016/S1571-0661(05)80265-8.
  17. Marina Lenisa, John Power, and Hiroshi Watanabe. Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. Electronical Notes in Computer Science, 33:230-260, 2000. URL: https://doi.org/10.1016/S1571-0661(05)80350-0.
  18. S. Milius, L. S. Moss, and D. Schwencke. Abstract GSOS rules and a modular treatment of recursive definitions. Logical Methods in Computer Science, 9(3), 2013. URL: https://doi.org/10.2168/LMCS-9(3:28)2013.
  19. R. Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  20. Ernst-Rüdiger Olderog and C. A. R. Hoare. Specification-oriented semantics for communicating processes. Acta Inf., 23(1):9-66, 1986. Google Scholar
  21. D. Park. A new equivalence notion for communicating systems. In G. Maurer, editor, Bulletin EATCS, volume 14, pages 78-80, 1981. Abstract of the talk presented at the Second Workshop on the Semantics of Programming Languages, Bad Honnef, March 16-20 1981. Abstracts collected in the Bulletin by B. Mayoh. Google Scholar
  22. Iain Phillips. Refusal testing. Theor. Comput. Sci., 50:241-284, 1987. A preliminary version in Proc. ICALP'86, Lecture Notes in Computer Science 226, Springer Verlag. Google Scholar
  23. A. Pnueli. Linear and branching structures in the semantics and logics of reactive systems. In W. Brauer, editor, 12th ICALP, volume 194 of Lecture Notes in Computer Science, pages 15-32. Springer Verlag, 1985. Google Scholar
  24. Lucia Pomello. Some equivalence notions for concurrent systems. an overview. In Grzegorz Rozenberg, editor, Advances in Petri Nets 1985, volume 222 of Lecture Notes in Computer Science, pages 381-400. Springer, 1985. URL: https://doi.org/10.1007/BFb0016202.
  25. D. Pous. Complete lattices and up-to techniques. In Proc. APLAS '07, volume 4807 of Lecture Notes in Computer Science, pages 351-366. Springer Verlag, 2007. URL: https://doi.org/10.1007/978-3-540-76637-7_24.
  26. Damien Pous. Coinduction all the way up. In Proc. LICS, pages 307-316. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934564.
  27. Damien Pous and Jurriaan Rot. Companions, Codensity, and Causality. In Proc. FoSSaCS, volume 10203 of Lecture Notes in Computer Science, pages 106-123. Springer Verlag, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_7.
  28. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan Rutten, editors, Advanced Topics in Bisimulation and Coinduction. Cambridge University Press, 2012. Google Scholar
  29. Damien Pous and Davide Sangiorgi. Bisimulation and coinduction enhancements: A historical perspective. Formal Asp. Comput., 31(6):733-749, 2019. URL: https://doi.org/10.1007/s00165-019-00497-w.
  30. Jurriaan Rot, Filippo Bonchi, Marcello M. Bonsangue, Damien Pous, Jan Rutten, and Alexandra Silva. Enhanced coalgebraic bisimulation. Mathematical Structures in Computer Science, 27(7):1236-1264, 2017. URL: https://doi.org/10.1017/S0960129515000523.
  31. D. Sangiorgi. On the bisimulation proof method. Journal of Mathematical Structures in Computer Science, 8:447-479, 1998. URL: https://doi.org/10.1017/S0960129598002527.
  32. D. Sangiorgi and R. Milner. The problem of "Weak Bisimulation up to". In W.R. Cleveland, editor, Proc. CONCUR '92, volume 630 of Lecture Notes in Computer Science, pages 32-46. Springer Verlag, 1992. URL: https://doi.org/10.1007/BFb0084781.
  33. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2012. URL: https://doi.org/10.1017/CBO9780511777110.
  34. Davide Sangiorgi. Equations, contractions, and unique solutions. ACM Trans. Comput. Log., 18(1):4:1-4:30, 2017. URL: https://doi.org/10.1145/2971339.
  35. Davide Sangiorgi. From enhanced coinduction towards enhanced induction. Proc. ACM Program. Lang., 6(POPL):1-29, 2022. URL: https://doi.org/10.1145/3498679.
  36. A. Silva, F. Bonchi, M. Bonsangue, and J. Rutten. Generalizing the powerset construction, coalgebraically. In FSTTCS, LIPIcs, pages 272-283. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.272.
  37. Tarmo Uustalu, Varmo Vene, and Alberto Pardo. Recursion schemes from comonads. Nord. J. Comput., 8(3):366-390, 2001. URL: http://www.cs.helsinki.fi/njc/References/uustaluvp2001:366.html.
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