Branching-Time Semantics

Context

Goranko2023 - Temporal Logics distinguishes linear-time semantics from branching-time semantics, then separates two classical branching-time readings: Peircean and Ockhamist. This annex keeps those semantic clauses in one place so the main source and concept notes can stay navigational.

Formal Statement

A branching-time structure is a tree-like temporal frame T = <T, prec>, where prec is a backward-linear partial order and any two instants have a common predecessor. A history is a maximal linearly ordered subset of T; H(t) is the set of histories passing through instant t.

For a Peircean model M = <T, prec, V>, truth is evaluated at instants. The future operators quantify over histories through the current instant:

$$M,t\models F\varphi ⟺\forall h\in H(t)\exists t^{\prime }\in h.t\prec t^{\prime }\wedge M,t^{\prime }\models \varphi .$$ $$M,t\models G\varphi ⟺\forall h\in H(t)\forall t^{\prime }\in h.t\prec t^{\prime }\Rightarrow M,t^{\prime }\models \varphi .$$

The dual weak operators are f phi := not G not phi and g phi := not F not phi.

For an Ockhamist model, truth is evaluated at a branch (h,t) with h in H(t). The temporal operators move along the selected history, while modal operators quantify over alternative histories through the same instant:

$$M,(h,t)\models F\varphi ⟺\exists t^{\prime }\in h.t\prec t^{\prime }\wedge M,(h,t^{\prime })\models \varphi .$$ $$M,(h,t)\models ◊\varphi ⟺\exists h^{\prime }\in H(t).M,(h^{\prime },t)\models \varphi .$$ $$M,(h,t)\models \square \varphi ⟺\forall h^{\prime }\in H(t).M,(h^{\prime },t)\models \varphi .$$

The corresponding G, P, and H clauses are the expected universal future, existential past, and universal past operators along the selected history.

Derivation / Construction

• Linear-time logic is recovered when the current model has only one relevant history through each instant.
• Peircean F phi means that phi eventually holds on every possible future, with no privileged actual future.
• Ockhamist F phi means that phi eventually holds on the selected actual history; Diamond F phi and Box F phi expose possible and necessary future eventuality.
• CTL can be seen as a computation-tree specialization that pairs path quantifiers with X, G, and U, for example forall X phi or exists(phi U psi).
• CTL* uses the Ockhamist style over omega-trees but allows freer nesting of path quantifiers and LTL temporal operators.
• Peircean formulas embed into Ockhamist syntax by treating instant atoms as history-invariant and translating strong future operators as tau(F phi) = Box F tau(phi) and tau(G phi) = Box G tau(phi).

Implications

• Branching-time semantics clarify future-contingent statements: “will happen” can mean inevitable across all histories, true on a selected history, or possible on at least one history.
• For verification, the semantic choice determines whether specifications are trace properties, tree properties, or strategy/probability properties layered on top of trees.
• For multi-agent settings, branching-time logic is a stepping stone from path quantification to richer notions such as coalition ability in Alternating-Time Temporal Logic or probabilistic strategic thresholds in Probabilistic Strategic Timed CTL.

Links

• Branching-Time Temporal Logic
• Goranko2023 - Temporal Logics
• Linear Temporal Logic
• Temporal Logic
• Formal Methods