Document Open Access Logo

Generic Trace Semantics and Graded Monads

Authors Stefan Milius, Dirk Pattinson, Lutz Schröder

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2015.253.pdf
  • Filesize: 475 kB
  • 17 pages

Document Identifiers

Author Details

Stefan Milius
Dirk Pattinson
Lutz Schröder

Cite As Get BibTex

Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic Trace Semantics and Graded Monads. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 253-269, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CALCO.2015.253

Abstract

Models of concurrent systems employ a wide variety of semantics inducing various notions of process equivalence, ranging from linear-time semantics such as trace equivalence to branching-time semantics such as strong bisimilarity. Many of these generalize to system types beyond standard transition systems, featuring, for example, weighted, probabilistic, or game-based transitions; this motivates the search for suitable coalgebraic abstractions of process equivalence that cover these orthogonal dimensions of generality, i.e. are generic both in the system type and in the notion of system equivalence. In recent joint work with Kurz, we have proposed a parametrization of system equivalence over an embedding of the coalgebraic type functor into a monad. In the present paper, we refine this abstraction to use graded monads, which come with a notion of depth that corresponds, e.g., to trace length or bisimulation depth. We introduce a notion of graded algebras and show how they play the role of formulas in trace logics.

Subject Classification

Keywords
  • transition systems
  • monads
  • coalgebra
  • trace logics

Metrics

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

References

  1. Luca Aceto, Anna Ingólfsdóttir, Kim Larsen, and Jiři Srba. Reactive systems: modelling, specification and verification. Cambridge Univ. Press, 2007. Google Scholar
  2. Jiř\'ıAdámek, Jiř\'ıRosický, and Enrico Vitale. Algebraic Theories. Cambridge Univ. Press, 2011. Google Scholar
  3. Marco Bernardo and Stefania Botta. A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems. Math. Struct. Comput. Sci., 18:29-55, 2008. Google Scholar
  4. Nick Bezhanishvili and Silvio Ghilardi. The bounded proof property via step algebras and step frames. Ann. Pure Appl. Logic, 165:1832-1863, 2014. Google Scholar
  5. Marcello Bonsangue, Stefan Milius, and Alexandra Silva. Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log., 14, 2013. Google Scholar
  6. Ivan Christoff. Testing equivalences and fully abstract models for probabilistic processes. In Theories of Concurrency, CONCUR 1990, volume 458 of LNCS, pages 126-140. Springer, 1990. Google Scholar
  7. Corina Cîrstea. A coalgebraic approach to linear-time logics. In Foundations of Software Science and Computation Structures, FoSSaCS 2014, volume 8412 of LNCS, pages 426-440. Springer, 2014. Google Scholar
  8. Corina Cîrstea. Canonical coalgebraic linear time logics. In Proc. CALCO, 2015. This volume. Google Scholar
  9. Silvio Ghilardi. An algebraic theory of normal forms. Ann. Pure Appl. Logic, 71:189-245, 1995. Google Scholar
  10. Valentin Goranko and Martin Otto. Model theory of modal logic. In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, pages 249-329. Elsevier, 2006. Google Scholar
  11. Daniel Gorín and Lutz Schröder. Simulations and bisimulations for coalgebraic modal logics. In Algebra and Coalgebra in Computer Science, CALCO 2013, volume 8089 of LNCS, pages 253-266. Springer, 2013. Google Scholar
  12. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Meth. Comput. Sci., 3, 2007. Google Scholar
  13. Antony Hoare. Communicating sequential processes. Prentice Hall, 1985. Google Scholar
  14. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Coalgebraic Methods in Computer Science, CMCS 2012, volume 7399 of LNCS, pages 109-129. Springer, 2012. Google Scholar
  15. Peter Johnstone. Adjoint lifting theorems for categories of algebras. Bull. London Math. Soc., 7:294-297, 1975. Google Scholar
  16. Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Principles of Programming Languages, POPL 2014, pages 633-646. ACM, 2014. Google Scholar
  17. Christian Kissig and Alexander Kurz. Generic trace logics. arXiv preprint 1103.3239, 2011. Google Scholar
  18. Bartek Klin and Juriaan Rot. Coalgebraic trace semantics via forgetful logics. In Foundations of Software Science and Computation Structures, FoSSaCS'15, 2015. Google Scholar
  19. Alexander Kurz, Stefan Milius, Dirk Pattinson, and Lutz Schröder. Simplified coalgebraic trace equivalence. In Software, Services, and Systems, volume 8950 of LNCS, pages 75-90. Springer, 2015. Google Scholar
  20. A. Mazurkiewicz. Concurrent Program Schemes and Their Interpretation. Aarhus University, Comp. Sci. Depart., DAIMI PB-78, July 1977. Google Scholar
  21. P.-A. Mellies. The parametric continuation monad. Preprint, 2015. Google Scholar
  22. Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93:55-92, 1991. Google Scholar
  23. Philip Mulry. Lifting theorems for Kleisli categories. In Mathematical Foundations of Programming Semantics, MFPS 1993, volume 802 of LNCS, pages 304-319. Springer, 1994. Google Scholar
  24. D. Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Logic, 45:19-33, 2004. Google Scholar
  25. J. Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000. Google Scholar
  26. L. Schröder and D. Pattinson. PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log., 10:13:1-13:33, 2009. Google Scholar
  27. L. Schröder and D. Pattinson. Rank-1 modal logics are coalgebraic. J. Log. Comput., 20, 2010. Google Scholar
  28. Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390:230-247, 2008. Google Scholar
  29. Lutz Schröder and Dirk Pattinson. Coalgebraic correspondence theory. In Foundations of Software Structures and Computer Science, FoSSaCS 2010, volume 6014 of LNCS, pages 328-342. Springer, 2010. Google Scholar
  30. Alexandra Silva, Filippo Bonchi, Marcello Bonsangue, and Jan Rutten. Generalizing determinization from automata to coalgebras. Log. Meth. Comput. Sci, 9(1:9), 2013. Google Scholar
  31. A. Smirnov. Graded monads and rings of polynomials. J. Math. Sci., 151:3032-3051, 2008. Google Scholar
  32. Sam Staton. Relating coalgebraic notions of bisimulation. Log. Meth. Comput. Sci., 7, 2011. Google Scholar
  33. Rob van Glabbeek. The linear time-branching time spectrum (extended abstract). In Theories of Concurrency, CONCUR'90, volume 458 of LNCS, pages 278-297. Springer, 1990. Google Scholar
  34. James Worrell. On the final sequence of a finitary set functor. Theor. Comput. Sci., 338:184-199, 2005. 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