The temporal logic of coalgebras via Galois algebras. (English) Zbl 1030.03017

A temporal logic for coalgebras is introduced by defining nexttime and lasttime operators. The main contribution of this paper is to establish a connection beween coalgebras and temporal logic, by showing that each coalgebra gives rise to a Galois algebra (i.e. a complete Boolean algebra with a Galois connection). Some examples allow to appreciate how ubiquitous this structure is, for instance, in showing the fuzzy predicates on metric spaces, and predicates on presheaves, both yield indexed Galois algebras in basically the same coalgebraic manner. Technically, the paper shows how coalgebras of so-called polynomial functors on sets give rise to Galois algebras, making crucial use of {predicate lifting}. Later, it is shown how the temporal operators can also be defined pathwise, and give rise to Galois algebras as well. The study on Galois algebras is essentially based on B. von Karger’s paper “Temporal algebra” [Math. Struct. Comput. Sci. 8, 277-320 (1998; Zbl 0917.03011)] except for the part dealing with strict and affine lifting. Finally, the main summarizing result is presented: there is a functorial mapping from coalgebras to Galois algebras, yielding indexed categorical structures.


03B44 Temporal logic
03G30 Categorical logic, topoi
68Q60 Specification and verification (program logics, model checking, etc.)
03B70 Logic in computer science
06A15 Galois correspondences, closure operators (in relation to ordered sets)


Zbl 0917.03011


Isabelle; CCSL; PVS
Full Text: DOI