Towards Systematic Construction of Temporal Logics for Dynamical Systems via Coalgebra

Abstract

Temporal logics are an obvious high-level descriptive companion formalism to dynamical systems which model behavior as deterministic evolution of state over time. A wide variety of distinct temporal logics applicable to dynamical systems exists, and each candidate has its own pragmatic justification. Here, a systematic approach to the construction of temporal logics for dynamical systems is proposed: Firstly, it is noted that dynamical systems can be seen as coalgebras in various ways. Secondly, a straightforward standard construction of modal logics out of coalgebras, namely Moss’s coalgebraic logic, is applied. Lastly, the resulting systems are characterized with respect to the temporal properties they express.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Dynamical systems are the classical constructive formalism for behaviour arising from the deterministic evolution of system state over time [1], dating back to the works of Newton and Laplace. Clearly temporal logics, with operators such as ‘next’, ‘always’, ‘eventually’ and ‘for-at-least’, constitute a companion descriptive formalism. However, the relation is not one-to-one: One the one hand, there is a unifying theory underlying the various perspectives on dynamical systems as monoid actions, which uniformly covers discrete and continuous, as well as hybrid systems [6]. But on the other hand, the diversity of temporal logics in literature is immense, see [13], and the choice for a particular system is often justified by ad-hoc pragmatic arguments. The present article explores a potentially systematic approach to the construction of temporal logics for dynamical systems, via the relatively recent mathematical field of universal coalgebra which has been shown to be intimately connected to both dynamical systems [11] and modal logics [5]. A different approach, also based on coalgebras and the Stone duality, has been suggested [3] for constructing modal logics of transition systems, a close relative of dynamical systems from theoretical computer science.

The method outlined in the remainder of this article, while theoretically simple, touches on many different fields of mathematics: order theory, category theory, algebra, coalgebra, classical modal logics à la Kripke, and coalgebraic logics à la Moss [8]. Thus a significant fraction of this paper is dedicated to reviewing the relevant definitions and propositions from the respective standard literature. This review makes up the Sects. 2 and 3. The expert reader is encouraged to skip ahead: Sect. 4 ties up all the loose ends and gives a novel contribution. There a selection of obvious coalgebraic perspectives on dynamical systems is explored, and the respective logics entailed by applying Moss’s construction are characterized.

2 Review: Classical Ingredients

This section reviews some basic definitions and propositions.

2.1 Order Relations

We assume that the reader is familiar with basic order-theoretic properties of binary relations, namely with reflexive, transitive, symmetric relations, and with preorders, partial orders and equivalences. We give two additional related definitions that are not quite as universal:

Definition 1

(Non-Branching & Linear Relations). Let $X$ be a set. A binary relation $R \subseteq X^2$ is called

• non-branching if and only if $x \mathrel R y$ and $x \mathrel R z$ imply $y \mathrel R z$ or $z \mathrel R y$, and

• linear if and only if $x \mathrel R y$ or $y \mathrel R x$,

respectively, for all $x, y, z \in X$. Clearly, every linear relation is non-branching.

2.2 Monoids

We assume that the reader is familiar with the notions of a monoid $\mathbb M = (M, 0, +)$, and of monoid generators. We recall that every monoid induces an ordering relation:

Definition 2

(Monoid Order). Let $\mathbb M = (M, 0, {+})$ be a monoid. For any elements $a, b \in M$, we write $a \le _{\mathbb M} b$ if and only if there is some $c \in M$ such that $a + c = b$. We say that $a \le _{\mathbb M} b$ via $c$. It follows directly from the monoid axioms that $\le _{\mathbb M}$ is reflexive and transitive, and hence a preorder. By extension, $\mathbb M$ itself is called symmetric/non-branching/linear if and only if $\le _{\mathbb M}$ is symmetric/non-branching/linear, respectively.

Note that being symmetric in this sense is different from being Abelian. In fact, symmetry characterizes a famous subclass of monoids, namely the groups:

Lemma 1

(Groups). A monoid $\mathbb M$ is a group if and only if it is symmetric. Every symmetric monoid is trivially linear, with the degenerate order $(\le _{\mathbb M}) = M^2$, the full relation.

The proof of this simple but non-standard proposition is left as an exercise to the reader.

2.3 Dynamical Systems

Definition 3

(Dynamical System). Let $\mathbb T = (T, 0, {+})$ be a monoid called time (durations). A dynamical system is an enriched structure $\mathbb S = (\mathbb T, S, \varPhi )$ with

• a set $S$ called state space, and

• a map $\varPhi : S \times T \rightarrow S$ called dynamics,

such that

$$\begin{aligned} \varPhi (s, 0)&= s&\qquad \varPhi \bigl (\varPhi (s, t), u\bigr )&= \varPhi (s, t + u) \end{aligned}$$

In other words, $\varPhi$ is a right monoid action of $\mathbb T$ on $S$. $\mathbb S$ is called

• linear-time if and only if $\mathbb T$ is linear, otherwise nonlinear-time, and

• invertible if and only if $\mathbb T$ is symmetric.

Corollary 1

There are no invertible nonlinear-time dynamical systems.

Dynamical systems are a fundamental model class of many natural and social sciences. In comparison with their younger counterparts in computer science, automata and transition systems, dynamical systems are typically

• behaviourally weaker; deterministic, non-pointed (without distinguished initial states) and total (without spontaneous termination), but

• structurally stronger; with additional features of time (density, completeness) and state space (topology, metric, differential geometry, measures).

Automata-like constructions can be emulated by dynamical systems; see Example 1 below.

Definition 4

(Step, Trajectory & Orbit). From the dynamics map $\varPhi$ we may derive three forms of secondary maps:

$$\begin{aligned} \begin{array}{lll} \quad \varPhi ^t : S \rightarrow S &{}\qquad \varPhi _s : T \rightarrow S &{}\qquad \quad \quad \; \varPhi ^\circ : S \rightarrow \mathcal PS \\ \varPhi ^t(s) = \varPhi (s, t) &{}\quad \varPhi _s(t) = \varPhi (s, t) &{}\qquad \quad \varPhi ^\circ (s) = \mathrm {Img}(\varPhi _s\\ &{} &{}\quad \qquad \quad \quad \ \ \!\!\!= \{ \varPhi (s, t) \mid t \in T \} \end{array} \end{aligned}$$

• $\varPhi ^t$ is called the step of duration $t$, or just the $t$-step.

• $\varPhi _s$ is called the trajectory of initial state $s$.

• $\varPhi ^\circ (s)$ is called the orbit of state $s$.

Lemma 2

(Homomorphic Steps). The dynamical systems with time $\mathbb T$ are precisely those systems $(\mathbb T, S, \varPhi )$ such that the step construction is a monoid homomorphism from $\mathbb T$ into the monoid of maps of type $S \rightarrow S$ with right composition.

$$\begin{aligned} \varPhi ^0&= \mathrm {id}_S&\qquad \varPhi ^{t+u}&= \varPhi ^u \circ \varPhi ^t \end{aligned}$$

Corollary 2

(Generating Steps). If $G \subseteq T$ generates the monoid $\mathbb T$, then $\varPhi$ is determined uniquely by the collection of steps $(\varPhi ^t)_{t \in G}$.

Example 1

(Instances of Time)

• The time monoid $(\mathbb {N}, 0, +)$ yields standard non-invertible, linear-time, discrete-time dynamical systems. The step $\varPhi ^1$ is generating. Trajectories are (one-sided) infinite sequences.

• The time monoid $(\mathbb {Z}, 0, +)$ yields standard invertible, hence linear-time, discrete-time dynamical systems. The step $\varPhi ^1$ is generating and must be invertible. Trajectories are two-sided infinite sequences.

• The time monoid $(\mathbb {R}_+, 0, +)$ yields standard non-invertible, linear-time, continuous-time dynamical systems. No finite step generator collection exists. Trajectories are one-sided parametric curves.

• The time monoid $(\mathbb {R}, 0, +)$ yields standard invertible, hence linear-time, continuous-time dynamical systems. No finite step generator exists; classically definitions are given as solutions to ordinary differential equations. Trajectories are two-sided parametric curves.

• The free “time” monoid $(\varSigma ^*, \varepsilon , \cdot )$ over some finite alphabet $\varSigma$ yields total semiautomata, or deterministic finitely-labelled transition systems. The steps $\{\varPhi ^a \mid a \in \varSigma \}$ (columns of the transition table) are generating. Trajectories are big-step transition functions of total automata, mapping input words to final states.   $\square$

2.4 Propositional Modal Logics

We assume that the reader is familiar with the syntax and semantics of classical propositional logics and their presentation solely in terms of the connectives $\lnot$ and $\rightarrow$. For the modal extensions, see [2] or some other textbook.

Definition 5

(Syntax of Propositional Modal Logics). The modal extension of classical propositional logics adds two unary connectives $\Box$ and $\lozenge$, taking $\Box$ as primitive and defining

$$\begin{aligned} \lozenge A = \lnot \Box \lnot A \end{aligned}$$

Definition 6

(Semantics of Propositional Modal Logics). A normal modal extension of classical propositional logics adds at least the deduction rule of necessitation or generalization, and the axiom of distribution:

$$\begin{aligned} A \vdash \Box A&\qquad \quad \Box (A \rightarrow B) \rightarrow (\Box A \rightarrow \Box B) \end{aligned}$$

Example 2

Important normal modal logics are obtained by adding certain axioms:

• $\Box A \rightarrow A$ added to the minimal system results in the logic $T$.

• $\Box A \rightarrow \Box \Box A$ added to $T$ results in the logic $S4$.

• $\Box (\Box A \rightarrow B) \vee \Box (\Box B \rightarrow A)$ added to $S4$ results in the logic $S4.3$.

• $\lozenge A \rightarrow \Box \lozenge A$ added to $S4$ or $S4.3$ results in the logic $S5$.   $\square$

2.5 Kripke Semantics

Definition 7

(Kripke Frame). A Kripke frame is a structure $(W, R)$ with a set $W$ of worlds and a binary relation $R$ on $W$ called accessibility.

Definition 8

(Kripke Model). Let $(W, R)$ be a Kripke frame. A Kripke model (of propositional modal logic) is an extended structure $(W, R, \Vdash )$, where $\Vdash$ is a relation between $W$ and the language $Form$ of logical formulas, such that:

We say that $w$ satisfies $A$ in $(W, R, \Vdash )$ if and only if $w \Vdash A$.

Lemma 3

The satisfaction relation $\Vdash$ of a Kripke model is determined uniquely by the satisfaction of atomic propositions.

Definition 9

(Validity). A formula $A$ is called valid in

• a Kripke model $(W, R, {\Vdash })$ if and only if it is satisfied in all worlds $w \in W$,

• a Kripke frame $(W, R)$ if and only if it is valid in all Kripke models $(W, R, \Vdash )$,

• a class $C$ of Kripke frames if and only if it is valid in all members of $C$.

Definition 10

(Soundness/Completeness). A propositional modal logic $L$ is called, with respect to a class $C$ of Kripke frames,

• sound if and only if provability in $L$ implies validity in $C$, and

• complete if and only if validity in $C$ implies provability in $L$.

Theorem 1

The modal logics $S4$/$S4.3$/$S5$ are sound and complete for the classes of Kripke frames $(W, R)$ where $R$ is an arbitrary/non-branching/symmetric preorder, respectively.

Definition 11

(Finite Frame Property). A propositional modal logic $L$ is said to have the finite frame property, if and only if it is complete for a class of finite Kripke frames.

Theorem 2

The modal logics $S4$/$S4.3$/$S5$ have the finite frame property, for the finite-frame subclasses of the respective classes given in Theorem 1.

3 Review: Non-classical Ingredients

This section briefly reviews some definitions and propositions from categorial coalgebra and coalgebraic logics. See [11] and [7, 8], respectively, for full details.

3.1 Category Theory

We assume that the reader is familiar with basic endofunctors on the category $\mathbf {Set}$, in particular the identical functor $\mathrm {Id}$, the constant functor $\mathrm {Const}(C)$ for any object $C$, the covariant $\mathrm {Hom}$-functors and the covariant powerset functor $\mathcal P$. All functors considered in the following are tacitly $\mathbf {Set}$-endofunctors.

Definition 12

(Monotonic, Standard & Finitary Functors). As usual, a functor is called

• monotonic if and only if it preserves inclusions,

• standard if and only if it preserves inclusions and weak pullbacks, and

• finitary if and only if it is determined completely by its action on finite sets.

A standard, infinitary functor $F$ has a finitary restriction $F_{\omega }$ defined by

$$\begin{aligned} F_{\omega }X&= \textstyle \bigcup \{ FY \mid Y \subseteq X \wedge Y\ finite\}&F_{\omega }(h : X \rightarrow Y)&= F h |_{F_{\omega }X} \end{aligned}$$

Relation liftings for functors are conventionally defined in terms of span diagrams, but a pointwise notation will be more convenient for the following discussions:

Definition 13

(Relation Lifting). Let $F$ be a functor. Every relation $R \subseteq X \times Y$ has a lifting $F[R] \subseteq FX \times FY$ defined as the set of pairs $(\hat{x}, \hat{y})$ for which there is some $\hat{r} \in FR$ such that $(F \pi _1)(\hat{r}) = \hat{x}$ and $(F \pi _2)(\hat{r}) = \hat{y}$.

Example 3

The liftings for some basic functors are as follows:

• The identical functor lift a relation to itself: $x \mathrel {\mathrm {Id}[R]} y$ if and only if $x \mathrel R y$.

• A constant functor lifts to the identical relation: $c \mathrel {\mathrm {Const}(C)[R]} d$ if and only if $c = d$.

• $Y \mathrel {\mathcal P[R]} Z$ if and only if for all $y \in Y$ there is a $z \in Z$, and vice versa, such that $y \mathrel {R} z$.

• $f \mathrel {\mathrm {Hom}(C, -)[R]} g$ if and only if $f(c) \mathrel R g(c)$ for all $c \in C$.   $\square$

3.2 Universal Coalgebra

We assume that the reader is familiar with the notion of $F$-coalgebras for a functor $F$, their associated homomorphisms, $F$-bisimulations and $F$-bisimilarity.

Definition 14

(Parallel Coalgebra Composition). Coalgebras with the same carrier can be combined in parallel: Let $(X, f)$ be an $F$-coalgebra and $(X, g)$ be a $G$-coalgebra. Then $(X, \langle f, g \rangle )$ is an $(F \times G)$-coalgebra, where

$$\begin{aligned} \langle f, g \rangle (x) = \bigl (f(x), g(x)\bigr ) \end{aligned}$$

3.3 Moss’s Coalgebraic Logic

The idea of Moss’s coalgebraic logic [8] is to replace Kripe frames by $F$-coalgebras for some functor $F$, and to derive a universal and natural modality from $F$ itself:

Definition 15

(Moss’s Coalgebraic Logic, Abstractly). Fix a standard functor $F$. Extend the syntax of propositional logic by a pseudo-unary connective $\nabla _{}$ that, unlike the classical modalities like $\Box$, applies not to a single formula $A \in Form$ but to an expression of type either $\widehat{A} \in F( Form )$ or $\widehat{A} \in F_{\omega }( Form )$. For infinitary $F$ where the choice makes a difference, the cases are called infinitary and finitary $F$-coalgebraic logics, respectively. A Moss model is a structure $(X, f, \Vdash )$ where $(X, f)$ is an $F$-coalgebra and $\Vdash$ is a relation between coalgebra states and formulas, such that

as for Kripke models, but

$$\begin{aligned} x \Vdash \nabla _{}\widehat{A} \iff f(x) \mathrel {F[\Vdash ]} \widehat{A} \end{aligned}$$

Moss’s coalgebraic logic as presented here specifies satisfaction only up to atomic propositions, in analogy to Kripke frames. In Moss’s original presentation, the specification is unique, in analogy to Kripke models:

Definition 16

(Moss’s Coalgebraic Logic, Concretely). Let $(X, f)$ be an $F$-coalgebra. Let $s : X \rightarrow \mathcal P( Prop )$ be the map that assigns to each state $x \in X$ the desired set of valid atomic propositions. Then $(X, s)$ is a $\mathrm {Const}\bigl (\mathcal P( Prop )\bigr )$-coalgebra. For the parallel composite coalgebra $(X, g = \langle f, s \rangle )$, a unique Moss model is specified by the additional clause

$$\begin{aligned} x \Vdash A \iff A \in s(x) \qquad (A \in Prop ) \end{aligned}$$

The following two propositions state that traditional Kripke frames are essentially equivalent to the special case $F = \mathcal P$:

Lemma 4

$\mathcal {P}$-coalgebras $(X, f)$ are in one-to-one correspondence to relations $R$ on $X$ by putting $x \mathrel {R} y$ if and only if $y \in f(x)$.

Theorem 3

The Kripke modalities $\Box , \lozenge$ and the Moss modality $\nabla _{}$ for finitary $\mathcal P$-coalgebraic logics are equivalent. For infinitary $\mathcal P$-coalgebraic logics, they are also equivalent in the presence of infinitary conjunction and disjunction; otherwise $\nabla _{}$ is generally more expressive.

$$\begin{aligned}&w \Vdash _{\mathrm K} \Box A \iff w \Vdash _{\mathrm M} \nabla _{}\{ A \} \vee \nabla _{}\emptyset&w \Vdash _{\mathrm K} \lozenge A \iff w \Vdash _{\mathrm M} \nabla _{}\{ A, \top \} \\&w \Vdash _{\mathrm M} \nabla _{}\widehat{A} \iff w \Vdash _{\mathrm K} \Box \bigl ({\textstyle \bigvee \widehat{A}}\bigr ) \wedge {\textstyle \bigwedge \lozenge \widehat{A}}&where\quad \lozenge \widehat{A} = \{ \lozenge B \mid B \in \widehat{A} \} \end{aligned}$$

where $\Vdash _{\mathrm K}$/$\Vdash _{\mathrm M}$ denote satisfaction à la Kripke/Moss, respectively.

In general, the infinitary version of the operator $\nabla _{}$ is better matched with a logic where conjunction and disjunction are also infinitary. While an uncommon topic classically, infinitary logics are an important topic in modal logic because of their connection to bisimulations; they always satisfy the Henessy–Milner property:

Theorem 4

(Expressivity). In any fully ($\wedge , \vee , \nabla _{}$)-infinitary $F$-coalgebraic logic, two states $s, t \in S$ satisfy the same set of formulas if and only if they are bisimilar.

Generally finitary logics are nicer to work with, and of course more likely to be decidable. See Example 5 below for popular temporal operators that are not finitary in this framework.

4 Constructions

This section gives novel theoretical results by investigating the ramifications of the following recipe:

• 1. identify some generic $F$-coalgebraic view on dynamical systems;

• 2. use Moss’s construction to obtain logics with $\nabla _{F}$ modality, depending on the functor $F$;

• 3. relate $\nabla _{F}$ to established temporal logic operators.

Note that all of the following constructions have the state space $S$ of a fixed dynamical system as the carrier of some coalgebra for various standard functors. Hence the associated logical languages can coexist naturally in a single system, by the parallel composition given in Definition 14.

4.1 Step Logics

Definition 17

(Step Coalgebra). Let $\mathbb S = (\mathbb T, S, \varPhi )$ be a dynamical system. For any element $t \in T$, the $\mathrm {Id}$-coalgebra $(S, \varPhi ^t)$ is called the $t$-step coalgebra of $\mathbb S$.

Definition 18

(Multistep Coalgebra). Let $\mathbb S = (\mathbb T, S, \varPhi )$ be a dynamical system. For any subset $U \subseteq T$, the $\mathrm {Hom}(U, -)$-coalgebra $(S, s \mapsto \varPhi _s \circ \mathrm {in})$, given the inclusion map $\mathrm {in} : U \rightarrow T$, is called the $U$-multistep coalgebra of $\mathbb S$.

Lemma 5

The $\nabla _{}$ modality of step coalgebras amounts to

• for the $t$-step:

  $$\begin{aligned} s \Vdash \nabla _{}A \iff \varPhi (s, t) \Vdash A \end{aligned}$$

• for the $U$-multistep:

  $$\begin{aligned} s \Vdash \nabla _{}\widehat{A} \iff \varPhi (s, t) \Vdash \widehat{A}(t)\ for\ all\ t \in U \end{aligned}$$

The functors for $t$-steps and finite $U$-multisteps are finitary; hence no additional distinction between finitary and infinitary logics arises.

Definition 19

(Step Modality). We define the temporal modality $\bigcirc$, with the intuitive meaning next, in terms of $\nabla _{}$.

$$\begin{aligned} \bigcirc A&= \nabla _{}A&\bigcirc _t A&= \nabla _{}u \mapsto {\left\{ \begin{array}{ll} A &{} (t = u) \\ \top &{} (t \ne u) \end{array}\right. } \end{aligned}$$

Example 4

(Multi-)Step coalgebras are of particular interest for finite generators, since they specify the dynamics uniquely and concisely. The following are generating in the sense of Example 1:

• For time $(\mathbb N, 0, +)$, the $1$-step coalgebra maps every state to its successor. The resulting temporal logic has $\bigcirc$ as the next operator of traditional unidirectional discrete-time temporal logic.

• For time $(\mathbb Z, 0, +)$, the $(\pm 1)$-multistep coalgebra maps every state to its successor/predecessor, respectively. The resulting temporal logic has $\bigcirc _{\pm 1}$ as the next/previously operators of traditional bidirectional discrete-time temporal logic, respectively.

• For “time” $(\varSigma ^*, \varepsilon , \cdot )$, the $\varSigma$-multistep coalgebra maps every automaton state to its response function (row of the transition table). The resulting logic has $(\bigcirc _a)_{a\in \varSigma }$ as the generating cases of Pratt’s necessity operators $[a]$ in dynamic logic [10], where they are extended to the free Kleene algebra over $\varSigma$.

Interesting infinite, non-generating examples include:

• For time $(\mathbb R, 0, +)$ and $\delta > 0$, let $U$ denote the open interval $(-\delta , \delta )$. The $U$-multistep coalgebra maps every state to its temporal $\delta$-neighbourhood.   $\square$

Step generators benefit from Moss’s Expressivity Theorem 4:

Corollary 3

The modality $\nabla _{}$ and the family of modalities $(\bigcirc _t)_{t \in U}$ for generating $U$ are straightforwardly equivalent if $U$ is finite, and equivalent in the presence of infinitary conjunction otherwise.

$$\begin{aligned} x \Vdash \nabla _{}\widehat{A} \iff x \Vdash \bigwedge _{t \in U} \bigcirc _t \widehat{A}(t) \end{aligned}$$

The following construction is the multistep limit case $U = T$.

4.2 Trajectory Logics

Definition 20

(Trajectory Coalgebra). Let $\mathbb S = (\mathbb T, S, \varPhi )$ be a dynamical system. The $\mathrm {Hom}(T, -)$-coalgebra $(S, s \mapsto \varPhi _s)$ is called the trajectory coalgebra of $\mathbb S$.

Lemma 6

The $\nabla _{}$ modality of trajectory coalgebras amounts to

$$\begin{aligned} s \Vdash \nabla _{}\widehat{A} \iff \varPhi (s, t) \Vdash \widehat{A}(t)\ for\ all\ t \in T \end{aligned}$$

The $\nabla _{}$ trajectory modality is a surprisingly powerful logical operator, with the severe disadvantage that there is no canonical syntactic representation. The following examples are but a small subset of useful special cases.

Example 5

Arguments of the $\nabla _{}$ trajectory modality are maps of type $T \rightarrow Form$. Various intensional notations for such maps, or time-dependent formulas, give rise to well-known temporal operators. Note that all following examples work for finitary $\nabla _{}$.

• Consider discrete time $(\mathbb N, 0, +)$ or $(\mathbb Z, 0, +)$. Define a zip operator

  $$\begin{aligned} A \leftrightharpoons B = \nabla _{}t \mapsto {\left\{ \begin{array}{ll} A &{} t\ \text {even} \\ B &{} t\ \text {odd} \end{array}\right. } \end{aligned}$$

  Then a dynamic system is bipartite, with characteristic formula $A$, if and only if $(A \leftrightharpoons \lnot A) \vee (\lnot A \leftrightharpoons A)$ is valid in the Moss model associated with its trajectories.

• Consider automaton time $(\varSigma ^*, \varepsilon , \cdot )$. Define a consumption operator

  $$\begin{aligned} eat (L, A, B) = \nabla _{}t \mapsto {\left\{ \begin{array}{ll} A &{} t \in L \\ B &{} t \not \in L \end{array}\right. } \end{aligned}$$

  for languages $L \subseteq \varSigma ^*$ and formulas $A, B$. Now let $A$ be a formula characterizing accepting states. Then an automaton, as a dynamical system, accepts at least/exactly the language $L \subseteq \varSigma ^*$ if and only if $eat (L, A, \top )$/$eat (L, A, \lnot A)$, respectively, is valid for its initial state(s) in the Moss model associated with its trajectories.

• Consider time with a linear antisymmetric order $<$. Define a change operator

  $$\begin{aligned} chg (t, A, B, C) = \nabla _{}u\mapsto {\left\{ \begin{array}{ll} A &{} u < t \\ B &{} u = t \\ C &{} u > t \end{array}\right. } \end{aligned}$$

  for time duration $t$ and formulas $A, B, C$. Then minimum/maximum-duration operators can be defined directly, in two variants differing in the inclusion of boundary cases:

  $$\begin{aligned} \mathrm {min}\, t.\; A&= chg (t, A, \top , \top )&\mathrm {max}\, t.\; A&= chg (t, \top , \top , \lnot A) \\ \mathrm {min}'\, t.\; A&= chg (t, A, A, \top )&\mathrm {max}'\, t.\; A&= chg (t, \top , \lnot A, \lnot A) \end{aligned}$$

  Imprecise operators such as until can be expressed as infinitary disjunctions:

  $$\begin{aligned} A \mathbin {\mathbf {U}} B = \bigvee _{t \in T} chg (t, A, B, \top ) \end{aligned}$$

4.3 Orbit Logics

The following construction shifts the coalgebraic focus from trajectories to orbits which are images of trajectories, hence abstracting from durations. The result is a family of qualitative temporal logics that can be expressed naturally in the classical modal operators, uniformly for all kinds of time structure:

Definition 21

(Orbit Coalgebra). Let $\mathbb S = (\mathbb T, S, \varPhi )$ be a dynamical system. The $\mathcal P$-coalgebra $(S, \varPhi ^\circ )$ is called the orbit coalgebra of $\mathbb S$. We say that in $\mathbb S$, $y$ is reachable from $x$, written $x \leadsto _{\mathbb S} y$, if and only if $y \in \varPhi ^\circ (x)$. More precisely, we say $x \leadsto _{\mathbb S} y$ via $t$, if and only if $y = \varPhi ^t(x)$.

Clearly, $x \leadsto _{\mathbb S} y$ if and only if there is some witness $t \in T$ such that $x \leadsto _{\mathbb S} y$ via $t$.

Lemma 7

For dynamical systems $\mathbb S$, the reachability relation $\leadsto _{\mathbb S}$ is

• 1. always a preorder,

• 2. additionally non-branching, but not generally linear, if $\mathbb S$ is linear-time, and

• 3. additionally symmetric if $\mathbb S$ is invertible.

Proof

• 1. Reflexivity and transitivity follow directly from the monoid axioms: $x \leadsto _{\mathbb S} x$ via $0$, and if $x \leadsto _{\mathbb S} y$ via $t$ and $y \leadsto _{\mathbb S} z$ via $u$, then $x \leadsto _{\mathbb S} z$ via $t + u$.

• 2. Assume that $x \leadsto _{\mathbb S} y$ via $t$ and $x \leadsto _{\mathbb S} z$ via $u$. By linearity of $\mathbb T$ assume, without loss of generality, that $t \le _{\mathbb T} u$ via $v$. Then $y \leadsto _{\mathbb S} z$ via $v$.

• 3. For symmetric $\mathbb T$, if $x \leadsto _{\mathbb S} y$ via $t$, then $y \leadsto _{\mathbb S} x$ via $-t$.   $\square$

The caveat in case 2 of this proposition is necessary:

Example 6

(Nonlinear Linear-Time Dynamical System). Set $T = \{0\}$, giving rise to the singleton monoid which is trivially linear. This fixes $\varPhi$ completely as $\varPhi (s, t) = \varPhi (s, 0) = s$, giving rise to a “still-life” structure of time. Then neither $x \leadsto _{\mathbb S} y$ nor $y \leadsto _{\mathbb S} x$ for $x \ne y$.

Definition 22

(Orbital Frame). A Kripke frame is called orbital if and only if it corresponds, in the sense of Lemma 4, to the orbit coalgebra of some dynamical system. An orbital frame is called linear-time/invertible if and only if it corresponds to the orbit coalgebra of some linear-time/invertible dynamical system, respectively.

Using this definition, Lemma 7 extends to Kripke frames:

Lemma 8

For any orbital Kripke frame $\mathbb F = (W, R)$, the relation $R$ is

• 1. always a preorder,

• 2. additionally non-branching if $\mathbb F$ is linear-time,

• 3. additionally symmetric if $\mathbb F$ is invertible.

This statement has a partial, finitary converse, which is by far the most technical result of the present paper:

Lemma 9

A finite Kripke frame $(W, R)$ is

• 1. always orbital if $R$ is a preorder,

• 2. additionally linear-time if $R$ is non-branching,

• 3. additionally invertible if $R$ is symmetric.

Proof

Construct a dynamical system $\mathbb S = (\mathbb T, S, \varPhi )$ with $(\leadsto _{\mathbb S}) = R$. In any case, clearly $S = W$. Proceed in reverse order and increasing flexibility of cases. For the latter two, consider the partition of $W$ into strongly connected components (sccs) of the preorder $R$: nonempty, maximal subsets $C \subseteq W$ such that $x \mathrel R y$ for all $x, y \in C$. We write $x \sim y$ if and only if $x, y$ are in the same scc, that is $x \mathrel R y$ and $y \mathrel R x$.

• 3. Set $\mathbb T = (\mathbb Z, 0, +)$. By symmetry of $R$ there are no related pairs across sccs. For each scc $C$ choose an arbitrary cyclic permutation. Set $\varPhi ^1$ to their union. Then

  • $x \leadsto _{\mathbb S} y$ via some $i < k$, where $k$ is the size of the scc containing both, if $x \mathrel R y$, and

  • otherwise .

• 2. Set $\mathbb T = (\mathbb N, 0, +)$. We say that $y$ is a successor of $x$, writing $x \ll y$, if and only if $x \mathrel R y$ but not $y \mathrel R x$. Clearly, $x \mathrel R y$ if and only if either $x \sim y$ or $x \ll y$, exclusively. We say that $x$ is transient if it has successors. Since $W$ is finite and $R$ is non-branching, every transient $x$ has a unique scc of least successors, from which we may choose one, say $x'$, and all elements reachable from $x$ are successors. Set $\varPhi ^1(x) = x'$. For non-transient $x$, all elements reachable from $x$ are in the same scc. Proceed as above. Then

  • $x \leadsto _{\mathbb S} y$ via some $i < k$, where $k$ is the number of successors of $x$, if $x \ll y$,

  • $x \leadsto _{\mathbb S} y$ via some $i < k$, where $k$ is the size of the scc containing both, if $x \sim y$, and

  • otherwise .

• 1. There are in general no least successors, and there may be non-successors reachable from transient elements. A more basic construction is needed: Set $\mathbb T = (\mathbb N^*, \varepsilon , \cdot )$, the free monoid over $\mathbb N$. For each $x \in W$ choose some infinite sequence $y = (y_0, y_1, \ldots ) \in W^\omega$ such that $x \mathrel R z$ if and only if $z = y_i$ for some $i$. This is always possible by invocation of countable choice, since the set $\{ z \mid x \mathrel R z\}$ is finite and nonempty. For the generating steps $\{ \varPhi ^n \mid n \in \mathbb N\}$, set $\varPhi ^n(x) = y_n$. Then

  • $x \leadsto _{\mathbb S} y$ via $1$, if $x \mathrel R y$, and

  • otherwise .   $\square$

Theorem 5

The modal logics $S4$/$S4.3$/$S5$ are sound and complete for arbitrary/linear-time/invertible orbital frames, respectively.

Proof

$S4$/$S4.3$/$S5$ are sound for the class of Kripke frames $(W, R$) where $R$ is an arbitrary/non-branching/symmetric preorder, respectively. By Lemma 8, they are also sound for the subclasses of arbitrary/linear-time/invertible orbital frames, respectively.

Conversely, $S4$/$4.3$/$S5$ are complete for the class of Kripke frames $(W, R$) where $R$ is an arbitrary/non-branching/symmetric preorder, respectively, and have the finite frame property. By Lemma 9, they are also complete for the subclasses of arbitrary/linear-time/invertible orbital frames, respectively.   $\square$

Example 7

The operators $\Box$ and $\lozenge$ are well-suited to express “long-term” behavioral properties of dynamical systems. For instance, let $A$ be the characteristic formula of a subset $U \subseteq S$ of the state space. Then $U$ is a stationary solution of a dynamical system if and only if $A \rightarrow \Box A$ is valid in the Moss model associated with its orbits.   $\square$

5 Conclusion and Outlook

Many operators discussed in the temporal logic literature can be subsumed under a common framework by viewing them as instances of Moss’s modality $\nabla _{}$, for some coalgebraic presentation of the underlying dynamical system models. As a rule of thumb,

• step coalgebras go with discrete time,

• trajectory coalgebras go with quantitative operators for either discrete or dense time, and

• orbit coalgebras go with arbitrary time and qualitative operators, in particular the classical modal operators and the framework of normal modal logics.

The examples given in this article are of course only a small selection to prove the viability of the approach. There is considerable potential for generalization. The trajectory modality is an extremely expressive tool, and it is likely that many other temporal operators can be shown to coincide with particular intensional notations for it. Besides, coalgebraic perspectives on dynamical systems other than the three detailed above could be considered. An interesting open problem and direction for future research is the integration of measure-theoretic temporal operators, for instance in duration calculus [4], into the framework.

Coalgebraic modal logics from predicate liftings [9] are an alternative to Moss’s logic, with somewhat different properties. A study of the predicate liftings arising from the functorial perspective on dynamical systems is expected provide some interesting additional insights.

Recently, some progress has been made in the use of non-standard analysis to clarify the relationship of discrete-time and continuous-time systems, in a way that is compatible with a coalgebraic perspective [12]. That approach might also be helpful in bridging the gap between our trajectory and orbit logics.