Maximal traces and path-based coalgebraic temporal logics
type: Item
instance of: scholarly article
title: Maximal traces and path-based coalgebraic temporal logics
zbMATH Open document ID: 1254.68147
author: Corina Cîrstea
published in: Theoretical Computer Science
publication date: 2011-09-22T00:00:00Z
review text: Coalgebraic logic serves as a generic framework for modal logics with a generalized semantics that may go well beyond the classical relational realm, including, e.g., probabilistic, preferential, game-oriented, or neighbourhood-based systems [the author, \textit{A. Kurz}, \textit{D. Pattinson}, \textit{L. Schröder} and \textit{Y. Venema}, ``Modal logics are coalgebraic'', Comput. J. 54, No. 1, 31--41 (2011; \url{doi:10.1093/comjnl/bxp004})]. One part of the programme of coalgebraic logic is to extend its scope orthogonally to the coalgebraic dimension of generality, covering features that may be phrased independently of the underlying coalgebraic semantics such as nominals or fixed points. The work under review may be seen as a part of this program in that it contributes to the understanding of temporal logics that depend on a notion of path, such as CTL* or PCTL [\textit{H.~Hansson} and \textit{B.~Jonsson}, Formal Asp. Comput. 6, No. 5, 512--535 (1994; Zbl 0820.68113)]. The basic setup employed here is that of a coalgebra \(X \to TFX\), where \(T\) is a monad, the computation type, and \(F\) is a functor, the branching type. Typical examples for \(T\) include powerset (for classical non-determinism) and (sub-)distributions (for probabilistic computation), while typical choices for \(F\) are polynomial functors modelling various modes of labelling and branching. The notion of path is captured in several generic notions of trace including an important concept of maximal trace, defined for a coalgebra with carrier set \(X\) via a \(T\)-Kleisli map into the final \(X\times F\)-coalgebra. It is shown that CTL* and PCTL are indeed examples of the approach, with obvious adaptations necessary in the case of PCTL in order to deal with arising measure-theoretic issues.
reviewed by: Lutz Schröder
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 03B44
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 5949169
zbMATH Keywords: temporal logic
zbMATH Keywords: paths
zbMATH Keywords: coalgebra
zbMATH Keywords: distributive laws
zbMATH Keywords: traces
MaRDI profile type: Publication
full work available at URL: j.tcs.2011.04.025
OpenAlex ID: W2064284596
cites work: Generic Trace Semantics via Coinduction
cites work: A logic for reasoning about time and reliability
cites work: Universal coalgebra: A theory of systems
cites work: Expressive logics for coalgebras via terminal sequence induction
cites work: Modular construction of complete coalgebraic logics
cites work: Modular games for coalgebraic fixed point logics
cites work: EXPTIME Tableaux for the Coalgebraic μ-Calculus
cites work: Results on the propositional \(\mu\)-calculus
cites work: CTL\(^*\) and ECTL\(^*\) as fragments of the modal \(\mu\)-calculus
cites work: Trace semantics for coalgebras
cites work: Generic infinite traces and path-based coalgebraic temporal logics
cites work: “Sometimes” and “not never” revisited
cites work: Q3946875
cites work: Q4283467
cites work: Terminal Coalgebras for Measure-Polynomial Functors
cites work: Traces, Executions and Schedulers, Coalgebraically
cites work: Semantics of weakening and contraction
cites work: Algebra and Coalgebra in Computer Science
cites work: Q4530231
DOI: 10.1016/J.TCS.2011.04.025
description: scientific article; zbMATH DE number 5949169