Maximal traces and path-based coalgebraic temporal logics |
| |
Authors: | Corina Cîrstea |
| |
Affiliation: | University of Southampton, UK |
| |
Abstract: | This paper gives a general coalgebraic account of temporal logics whose semantics involves a notion of computation path. Examples of such logics include the logic CTL* for transition systems and the logic PCTL for probabilistic transition systems. Our path-based temporal logics are interpreted over coalgebras of endofunctors obtained as the composition of a computation type (e.g. non-deterministic or stochastic) with a general transition type. The semantics of such logics relies on the existence of execution maps similar to the trace maps introduced by Jacobs and co-authors as part of the coalgebraic theory of finite traces (Hasuo et al., 2007 1]). We consider finite execution maps derived from the theory of finite traces, and a new notion of maximal execution map that accounts for maximal, possibly infinite executions. The latter is needed to recover the logics CTL* and PCTL as specific path-based logics. |
| |
Keywords: | Coalgebra Trace semantics Computation path Temporal logic Non-determinism Probability |
本文献已被 ScienceDirect 等数据库收录! |