Document Open Access Logo

Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum

Authors Ulrich Dorsch, Stefan Milius, Lutz Schröder

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2019.36.pdf
  • Filesize: 486 kB
  • 16 pages

Document Identifiers

Author Details

Ulrich Dorsch
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Stefan Milius
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Lutz Schröder
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Funding

This work forms part of the DFG-funded project COAX (MI 717/5-2 and SCHR 1118/12-2).

Cite As Get BibTex

Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 36:1-36:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.CONCUR.2019.36

Abstract

State-based models of concurrent systems are traditionally considered under a variety of notions of process equivalence. In the case of labelled transition systems, these equivalences range from trace equivalence to (strong) bisimilarity, and are organized in what is known as the linear time - branching time spectrum. A combination of universal coalgebra and graded monads provides a generic framework in which the semantics of concurrency can be parametrized both over the branching type of the underlying transition systems and over the granularity of process equivalence. We show in the present paper that this framework of graded semantics does subsume the most important equivalences from the linear time - branching time spectrum. An important feature of graded semantics is that it allows for the principled extraction of characteristic modal logics. We have established invariance of these graded logics under the given graded semantics in earlier work; in the present paper, we extend the logical framework with an explicit propositional layer and provide a generic expressiveness criterion that generalizes the classical Hennessy-Milner theorem to coarser notions of process equivalence. We extract graded logics for a range of graded semantics on labelled transition systems and probabilistic systems, and give exemplary proofs of their expressiveness based on our generic criterion.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Theory of computation → Modal and temporal logics
Keywords
  • Linear Time
  • Branching Time
  • Monads
  • System Equivalences
  • Modal Logics
  • Expressiveness

Metrics

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

Related Versions

References

  1. Jirí Adámek and Václav Koubek. Remarks on Fixed Points of Functors. In Fundamentals of Computation Theory, FCT 1977, LNCS, pages 199-205. Springer, 1977. URL: https://doi.org/10.1007/3-540-08442-8_86.
  2. 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
  3. Mikołaj Bojańczyk, Bartek Klin, and Slawomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  4. Filippo Bonchi, Alexandra Silva, and Ana Sokolova. The Power of Convex Algebras. In Concurrency Theory, CONCUR 2017, volume 85 of LIPIcs, pages 23:1-23:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. Google Scholar
  5. Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The Theory of Traces for Systems with Nondeterminism and Probability. In Logic in Computer Science, LICS 2019. IEEE, 2019. Google Scholar
  6. Marcello Bonsangue, Stefan Milius, and Alexandra Silva. Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log., 14, 2013. Google Scholar
  7. Corina Cîrstea. Maximal traces and path-based coalgebraic temporal logics. Theoret. Comput. Sci., 412(38):5025-5042, 2011. URL: https://doi.org/10.1016/j.tcs.2011.04.025.
  8. 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
  9. Corina Cîrstea. Canonical Coalgebraic Linear Time Logics. In Algebra and Coalgebra in Computer Science, CALCO 2015, Leibniz International Proceedings in Informatics, 2015. Google Scholar
  10. Corina Cîrstea. From Branching to Linear Time, Coalgebraically. Fund. Inform., 150(3-4):379-406, 2017. URL: https://doi.org/10.3233/FI-2017-1474.
  11. Yuxin Deng, Rob van Glabbeek, Matthew Hennessy, and Carroll Morgan. Characterising Testing Preorders for Finite Probabilistic Processes. Log. Meth. Comput. Sci., 4(4), 2008. URL: https://doi.org/10.2168/LMCS-4(4:4)2008.
  12. Josee Desharnais, Abbas Edalat, and Prakash Panangaden. A Logical Characterization of Bisimulation for Labeled Markov Processes. In Logic in Computer Science, LICS 1998, pages 478-487. IEEE Computer Society, 1998. Google Scholar
  13. Ernst-Erich Doberkat. Eilenberg-Moore algebras for stochastic relations. Inf. Comput., 204(12):1756-1781, 2006. URL: https://doi.org/10.1016/j.ic.2006.09.001.
  14. Ernst-Erich Doberkat. Erratum and Addendum: Eilenberg-Moore algebras for stochastic relations. Inf. Comput., 206(12):1476-1484, 2008. URL: https://doi.org/10.1016/j.ic.2008.08.002.
  15. Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Graded Monads and Graded Logics for the Linear Time - Branching Time Spectrum, 2019. URL: http://arxiv.org/abs/1812.01317.
  16. Laurent Doyen, Thomas Henzinger, and Jean-François Raskin. Equivalence of Labeled Markov Chains. Int. J. Found. Comput. Sci., 19(3):549-563, 2008. URL: https://doi.org/10.1142/S0129054108005814.
  17. Uli Fahrenberg and Axel Legay. A Linear-Time-Branching-Time Spectrum of Behavioral Specification Theories. In Theory and Practice of Computer Science, SOFSEM 2017, volume 10139 of LNCS, pages 49-61. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-51963-0.
  18. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic Trace Semantics via Coinduction. Log. Meth. Comput. Sci., 3, 2007. URL: https://doi.org/10.2168/LMCS-3(4:11)2007.
  19. M. Hennessy and R. Milner. Algebraic Laws for Non-Determinism and Concurrency. J. ACM, 32:137-161, 1985. Google Scholar
  20. Bart Jacobs. Trace Semantics for Coalgebras. In J. Adámek and S. Milius, editors, Coalgebraic Methods in Computer Science, CMCS 2004, volume 106 of ENTCS, pages 167-184. Elsevier, 2004. URL: https://doi.org/10.1016/j.entcs.2004.02.031.
  21. Bart Jacobs. Convexity, Duality and Effects. In C.S. Calude and V. Sassone, editors, Proc. TCS 2010, volume 323 of IFIP AICT, pages 1-19, 2010. Google Scholar
  22. Bart Jacobs, Paul B. Levy, and Jurriaan Rot. Steps and Traces. In Corina Cîrstea, editor, Proc. CMCS 2018, volume 11202 of LNCS, pages 122-143. Springer, 2018. Google Scholar
  23. 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. URL: https://doi.org/10.1007/978-3-642-32784-1.
  24. Krzysztof Kapulkin, Alexander Kurz, and Jiri Velebil. Expressiveness of Positive Coalgebraic Logic. In Advances in Modal Logic, AiML 2012, pages 368-385. College Publications, 2012. Google Scholar
  25. Henning Kerstan and Barbara König. Coalgebraic Trace Semantics for Continuous Probabilistic Transition Systems. Log. Meth. Comput. Sci., 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:16)2013.
  26. Christian Kissig and Alexander Kurz. Generic Trace Logics. arXiv preprint 1103.3239, 2011. Google Scholar
  27. Bartek Klin. Structural Operational Semantics for Weighted Transition Systems. In Semantics and Algebraic Specification, volume 5700 of LNCS, pages 121-139. Springer, 2009. Google Scholar
  28. Bartek Klin and Juriaan Rot. Coalgebraic trace semantics via forgetful logics. In Foundations of Software Science and Computation Structures, FoSSaCS 2015, volume 9034 of LNCS, pages 151-166. Springer, 2015. Google Scholar
  29. K. Larsen and A. Skou. Bisimulation through probabilistic testing. Inf. Comput., 94:1-28, 1991. Google Scholar
  30. Saunders MacLane. Categories for the working mathematician. Springer, 2nd edition, 1998. Google Scholar
  31. Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic Trace Semantics and Graded Monads. In Algebra and Coalgebra in Computer Science, CALCO 2015, Leibniz International Proceedings in Informatics, 2015. Google Scholar
  32. Lawrence Moss and Ignacio Viglizzo. Final coalgebras for functors on measurable spaces. Inf. Comput., 204(4):610-636, 2006. URL: https://doi.org/10.1016/j.ic.2005.04.006.
  33. D. Pattinson. Expressive Logics for Coalgebras via Terminal Sequence Induction. Notre Dame J. Formal Log., 45:19-33, 2004. Google Scholar
  34. Benjamin Pierce. Basic category theory for computer scientists. MIT Press, 1991. Google Scholar
  35. J. Rutten. Universal Coalgebra: A Theory of Systems. Theoret. Comput. Sci., 249:3-80, 2000. Google Scholar
  36. Lutz Schröder. Expressivity of Coalgebraic Modal Logic: The Limits and Beyond. Theoret. Comput. Sci., 390:230-247, 2008. Google Scholar
  37. Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann. Nominal Automata with Name Binding. In Foundations of Software Science and Computation Structures, FOSSACS 2017, volume 10203 of LNCS, pages 124-142, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7.
  38. Roberto Segala and Nancy Lynch. Probabilistic Simulations for Probabilistic Processes. In Concurrency Theory, CONCUR 1994, volume 836 of LNCS, pages 481-496. Springer, 1994. URL: https://doi.org/10.1007/978-3-540-48654-1.
  39. Alexandra Silva, Filippo Bonchi, Marcello Bonsangue, and Jan Rutten. Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci, 9(1:9), 2013. Google Scholar
  40. A. Smirnov. Graded Monads and Rings of Polynomials. J. Math. Sci., 151:3032-3051, 2008. Google Scholar
  41. Natsuki Urabe and Ichiro Hasuo. Coalgebraic Infinite Traces and Kleisli Simulations. In Algebra and Coalgebra in Computer Science, CALCO 2015, volume 35 of LIPIcs, pages 320-335. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. Google Scholar
  42. R. van Glabbeek. The Linear Time - Branching Time Spectrum I; The Semantics of Concrete, Sequential Processes. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, pages 3-99. Elsevier, 2001. URL: https://doi.org/10.1016/B978-044482830-9/50019-9.
  43. Gerco van Heerdt, Justin Hsu, Joël Ouaknine, and Alexandra Silva. Convex Language Semantics for Nondeterministic Probabilistic Automata. In Theoretical Aspects of Computing. ICTAC 2018, volume 11187 of LNCS, pages 472-492. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02508-3.
  44. 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