Supplement to Temporal Logic

Supplement: Transition Semantics

Transition semantics, introduced in Rumberg (2016), defines a branching time temporal logic in which possible courses of events are modeled by chains of local future possibilities, i.e. by linearly ordered sets of transitions, rather than by histories. Whereas histories represent complete possible courses of events, sets of transitions can represent incomplete possible courses of events as well, which can then be extended towards the future, thereby enabling a dynamic picture of the interrelation of actuality, possibility, and time (for an intuitive introduction to transition semantics along these lines, see Rumberg 2019).

The notion of a transition employed here generalizes the notion of a transition prevalent in computer science. Intuitively, transitions capture the immediate possible future continuations of a branching point in a tree \(\mathcal{T} = \langle T,\prec\rangle\), and a transition is formally defined as a pair \(\langle t,H\rangle\) consisting of a branching point \(t\in T\) and an equivalence class \(H \subseteq \mathcal{H}(t)\) of undivided histories at \(t\) (where two histories \(h,h'\in \mathcal{H}(t)\) are said to be undivided at \(t\) iff \(h,h' \in \mathcal{H}(t')\) for some time instant \(t'\) such that \(t\prec t'\)). A backwards-linear strict partial ordering between transitions is obtained along the following lines: \(\langle t,H\rangle\) precedes \(\langle t',H'\rangle\) iff (\(t\prec t'\) and \(H'\subset H\)), and a possible course of events \(C\) is defined as a possibly non-maximal, downward-closed chain of transitions ordered by that relation. Note that to every possible course of events \(C\), there naturally corresponds a non-empty set of histories, namely, the set of histories allowed by \(C\), defined by \(\mathcal{H}(C) := \bigcap_{\langle t,H\rangle\in C} H\).

The transition language contains, in addition to temporal and modal operators, a so-called stability operator \(S\), which is interpreted as a universal quantifier over the possible future extensions of a given transition set. Given a set of atomic propositions \({PROP}\), the set of formulae of the transition language can be recursively defined as follows:

\[\varphi := p \in {PROP} \mid \bot \mid \neg\varphi \mid (\varphi \wedge \varphi) \mid P\varphi \mid F\varphi \mid G\varphi \mid \Diamond\varphi \mid S\varphi.\]

In transition semantics, formulae are evaluated in a model on a tree \(\mathcal{T} = \langle T,\prec\rangle\) at pairs \((t,C)\) consisting of a time instant \(t\in T\) and a possible course of events \(C\) compatible with that instant, i.e. \(\mathcal{H}(C) \cap \mathcal{H}(t) \neq \emptyset\). A transition tree model is a triple \(\mathcal{M} = \langle T,\prec,V\rangle\) where \(\mathcal{T} = \langle T,\prec\rangle\) is a tree and \(V\) is a valuation that assigns to every atomic proposition \(p \in {PROP}\) the set of pairs \((t,C)\) at which \(p\) is considered true. The truth of an arbitrary formula \(\varphi\) at an instant \(t\) with respect to a possible course of events \(C\) in a transition tree model \(\mathcal{M}\) is defined inductively as follows:

  • \(\mathcal{M},t,C \vDash p\)   iff   \((t,C) \in V(p)\), for \(p\in {PROP}\);
  • \(\mathcal{M},t,C \not\vDash \bot\);
  • \(\mathcal{M},t,C \vDash \neg\varphi\)   iff   \(\mathcal{M},t,C\not\vDash\varphi\);
  • \(\mathcal{M},t,C \vDash \varphi \wedge \psi\)   iff   \(\mathcal{M},t,C \vDash \varphi\) and \(\mathcal{M},t,C \vDash \psi\);
  • \(\mathcal{M},t,C \vDash P\varphi\)   iff   \(\mathcal{M},t',C \vDash\varphi\) for some time instant \(t'\) such that \(t'\prec t\);
  • \(\mathcal{M},t,C \vDash F\varphi\)   iff   for all histories \(h\in \mathcal{H}(C) \cap \mathcal{H}(t)\), there is some time instant \(t' \in h\) such that \(t \prec t'\) and \(\mathcal{M},t',C \vDash \varphi\);
  • \(\mathcal{M},t,C \vDash G\varphi\)   iff   for all histories \(h\in \mathcal{H}(C) \cap \mathcal{H}(t)\) and for all time instants \(t' \in h\) such that \(t \prec t'\), \(\mathcal{M},t',C \vDash \varphi\);
  • \(\mathcal{M},t,C \vDash \Diamond\varphi\)   iff   \(\mathcal{M},t,C' \vDash \varphi\) for some possible course of events \(C'\) such that \(\mathcal{H}(C') \cap \mathcal{H}(t) \neq \emptyset\);
  • \(\mathcal{M},t,C \vDash S\varphi\)   iff   \(\mathcal{M},t,C' \vDash \varphi\) for all possible courses of events \(C' \supseteq C\) such that \(\mathcal{H}(C') \cap \mathcal{H}(t) \neq \emptyset\).

Thus, a formula of the form \(F\varphi\) is true at an instant \(t\) with respect to a possible course of events \(C\) iff every history that passes through \(t\) and is allowed by \(C\) contains some later instant \(t'\) at which \(\varphi\) is true relative to \(C\). Note that, due to the relativization to the set of histories allowed by \(C\), the truth values of formulae about the future can change under extensions of the transition set \(C\), and the stability operator \(S\) captures this behavior. A formula \(\varphi\) is said to be stably true (stably false) at \((t,C)\) if it is true (false) at \(t\) with respect to all possible extensions of \(C\), i.e. no matter how the future unfolds later on. Formulae that are neither stably true nor stably false are contingent.

A formula of the transition language is valid iff it is true at all pairs \((t,C)\) in all transition tree models. While transition semantics validates the principle of excluded middle \(\varphi \vee \neg \varphi\), it invalidates the principle of future excluded middle \(F\varphi \vee F\neg\varphi\). However, the latter disjunction can only be contingently false: the scheme \(\neg S\neg (F\varphi \vee F\neg\varphi)\) is generally valid.

Both the Peircean and the Ockhamist branching time temporal logics can be obtained as limiting cases by restricting the range of possible courses of events to the empty set of transitions and maximal chains, respectively. To spell out the idea formally, we need to equip trees \(\mathcal{T} = \langle T,\prec\rangle\) with a primitive set of transition sets \(\mathit{TS}\) such that every time instant in \(\mathcal{T}\) belongs to a history allowed by some set of transitions in \(\mathit{TS}\). Peirceanism amounts to the case where \(\mathit{TS} = \{\emptyset\}\), whereas Ockhamism results if \(\mathit{TS} = \{C\mid C \text{ maximal linear}\}\). The corresponding classes of frames are definable by the formulae \(\varphi \leftrightarrow \Box \varphi\) and \(F\varphi \vee F\neg\varphi\), respectively.

Note that transition semantics is not a genuine Kripke-style semantics, i.e., formulae are not solely evaluated at time instants, which form the primitive elements of a tree, and the language contains intensional operators which are not interpreted along the temporal precedence relation between time instants. Rather, transition semantics makes use of a second, defined parameter of truth, and the transition sets employed as that second parameter are set-theoretically rather complex. In Rumberg and Zanardo (2019) it is shown that the set-theoretic complexity can be evaded: based on a one-to-one correspondence between transition sets and certain tree substructures, called prunings, a class of first-order definable Kripke structures with a genuine Kripke-style semantics is provided that preserves validity, which then naturally leads to axiomatizability results.

Copyright © 2020 by
Valentin Goranko <>
Antje Rumberg <>

Open access to the SEP is made possible by a world-wide funding initiative.
The Encyclopedia Now Needs Your Support
Please Read How You Can Help Keep the Encyclopedia Free