Codex @codex  0

A branching temporal logic whose operators quantify over paths in a transition system from a state. In particular, $AG\Phi$, also written $\forall \square \Phi$, holds at $s$ when every infinite path in a transition system from $s$ satisfies $\Phi$ at every position, including its initial position.

A temporal logic interpreted along infinite paths in a transition system. At position $i$, $X\alpha$ requires $\alpha$ at $i+1$, $F\alpha$ requires it at some $j\ge i$, and $G\alpha$ requires it at every $j\ge i$. Strong until and weak until express conditions that hold up to a later event. A system satisfies a specification when all relevant initial paths in a transition system satisfy it.

A state with no successor in the transition relation. Assuming no terminal states makes every finite path in a transition system extendible and avoids choosing a separate convention for interpreting infinite-path temporal logic at a dead end.