Maximal traces and path-based coalgebraic temporal logics (Q639645)

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.