License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CALCO.2015.66
URN: urn:nbn:de:0030-drops-55274
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5527/
Go to the corresponding LIPIcs Volume Portal

Cirstea, Corina

Canonical Coalgebraic Linear Time Logics

pdf-format:
6.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{cirstea:LIPIcs:2015:5527,
  author =	{Corina Cirstea},
  title =	{{Canonical Coalgebraic Linear Time Logics}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{66--85},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Lawrence S. Moss and Pawel Sobocinski},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5527},
  URN =		{urn:nbn:de:0030-drops-55274},
  doi =		{10.4230/LIPIcs.CALCO.2015.66},
  annote =	{Keywords: coalgebra, linear time logic, fixpoint logic}
}

Keywords: coalgebra, linear time logic, fixpoint logic
Collection: 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)
Issue Date: 2015
Date of publication: 28.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI