Document Open Access Logo

Canonical Coalgebraic Linear Time Logics

Author Corina Cirstea

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2015.66.pdf
  • Filesize: 0.55 MB
  • 20 pages

Document Identifiers

Author Details

Corina Cirstea

Cite As Get BibTex

Corina Cirstea. Canonical Coalgebraic Linear Time Logics. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 66-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CALCO.2015.66

Abstract

We extend earlier work on linear time fixpoint logics for coalgebras with branching, by showing how propositional operators arising from the choice of branching monad can be canonically added to these logics. We then consider two semantics for the uniform modal fragments of such logics: the previously-proposed, step-wise semantics and a new semantics akin to those of path-based logics. We prove that the two semantics are equivalent, and show that the canonical choice made for resolving branching in these logics is crucial for this property. We also state conditions under which similar, non-canonical logics enjoy the same property - this applies both to the choice of a branching modality and to the choice of linear time modalities. Our logics allow reasoning about linear time behaviour in systems with non-deterministic, probabilistic or weighted branching. In all these cases, the logics enhanced with propositional operators gain in expressiveness. Another contribution of our work is a reformulation of fixpoint semantics, which applies to any coalgebraic modal logic whose semantics arises from a one-step semantics.

Subject Classification

Keywords
  • coalgebra
  • linear time logic
  • fixpoint logic

Metrics

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

References

  1. Corina Cîrstea. From branching to linear time, coalgebraically. In Proceedings, FICS 2013, pages 11-27, 2013. Google Scholar
  2. Corina Cîrstea. A coalgebraic approach to linear-time logics. In Proceedings, FOSSACS 2014, pages 426-440, 2014. Google Scholar
  3. Corina Cîrstea and Dirk Pattinson. Modular construction of complete coalgebraic logics. Theor. Comput. Sci., 388(1-3):83-108, 2007. Google Scholar
  4. Dion Coumans and Bart Jacobs. Scalars, monads, and categories. In Quantum Physics and Linguistics. A Compositional, Diagrammatic Discourse, pages 184-216. Oxford Univ. Press, 2013. Google Scholar
  5. B.A. Davey and H.A. Priestley. Introduction to Lattices and Order (2. ed.). Cambridge University Press, 2002. Google Scholar
  6. Ichiro Hasuo. Generic weakest precondition semantics from monads enriched with order. In Proceedings, CMCS 2014, pages 10-32, 2014. Google Scholar
  7. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3(4), 2007. Google Scholar
  8. Michael Huth and Marta Z. Kwiatkowska. Quantitative analysis and model checking. In Proceedings, LICS 1997, pages 111-122, 1997. Google Scholar
  9. Bart Jacobs. Introduction to coalgebra. Towards mathematics of states and observations. Draft. Google Scholar
  10. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Proceedings, CMCS 2012, pages 109-129, 2012. Google Scholar
  11. Christian Kissig and Alexander Kurz. Generic trace logics. CoRR, abs/1103.3239, 2011. Google Scholar
  12. Bartek Klin and Jurriaan Rot. Coalgebraic trace semantics via forgetful logics. In Proceedings, FOSSACS 2015, pages 151-166, 2015. Google Scholar
  13. Anders Kock. Monads and extensive quantities, 2011. arXiv:1103.6009. Google Scholar
  14. Anders Kock. Commutative monads as a theory of distributions. Theory and Applications of Categories, 26(4):97-131, 2012. Google Scholar
  15. Clemens Kupke, Alexander Kurz, and Dirk Pattinson. Algebraic semantics for coalgebraic logics. Electr. Notes Theor. Comput. Sci., 106:219-241, 2004. Google Scholar
  16. Clemens Kupke, Alexander Kurz, and Yde Venema. Stone coalgebras. Theor. Comput. Sci., 327(1-2):109-134, 2004. Google Scholar
  17. Stefan Milius, Dirk Pattinson, and Lutz Schröder. Generic trace semantics and graded monads. This volume. 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