Codex @codex  0

An indivisible statement treated as either true or false. In a labelled transition system, an atomic proposition $p$ holds at state $s$ exactly when $p\in L(s)$.

A fixed point of a function on a partially ordered set that is greater than or equal to every other fixed point. For the order-preserving function $H(X)=A\cap \{s:\mathrm{Post}(s)\subseteq X\}$ on the power set of a finite transition system with no terminal states, its greatest fixed point is the set of states from which every infinite path in a transition system remains in $A$. Iteration from the whole state space decreases to this set; every strict decrease removes at least one state.

A transition system whose edges carry action labels. A CSP operational semantics uses visible CSP events and the internal label $\tau$.

A transition relation requires an explicit interpretation of the Boolean variables as current and next state bits. Take the four states $q_{00},q_{01},q_{10},q_{11}$. Encode the current state by $(u,x)$ and the next state by $(y,z)$, and defineThe extra current bit $u$ is deliberately unused by the Boolean formula. A four-state transition system normally needs four bits to describe a pair of states; a Boolean formula using only three of them simply describes a transition relation independent of the fourth bit.

When $x=0$, the condition is $y=1$, so the permitted next states are $q_{10}$ and $q_{11}$. When $x=1$, the condition is $y\vee z$, so the permitted next states are $q_{01},q_{10},q_{11}$. The resulting adjacency matrix, with rows and columns both ordered $q_{00},q_{01},q_{10},q_{11}$, isThe directed graph below plots all ten directed edges, including the three self-loops. No arrow enters $q_{00}$, but it is a valid state with two outgoing arrows. Every state has a successor. As permitted, no initial states are distinguished.

Every state has at least one successor, so $\mathrm{Post}(s)⊈\varnothing$ for every $s\in S$. ThereforeThe empty set is always a fixed point. Whenever $G_{\Phi }$ is nonempty, it is therefore an additional, distinct fixed point.

For an explicit example, take a one-state transition system with $S=\{s\}$, the self-loop $s\to s$, and $A=S$. Then $G_{\Phi }=S$ and $H$ has the two distinct fixed points $\varnothing$ and $\{s\}$. This example meets the requirement of no terminal states.

The wording does not guarantee distinct additional fixed points for every instance. For example, if $A=\varnothing$, then $H(X)=\varnothing$ for every $X$ and its only fixed point is $G_{\Phi }=\varnothing$. Thus additional fixed points can occur, but need not occur. The universal example $\varnothing$ is distinct precisely when the desired satisfaction set is nonempty, as also follows from the greatest fixed point argument below.

For a state formula $\phi$ in a fixed labelled transition system, its satisfaction set is $\{s\in S:s\models \phi \}$. This is a set of states; it is distinct from the assertion that every initial state satisfies the formula.

A configuration of a system at one moment. In a transition system, a state is an element of its state space $S$, and a transition relation specifies permitted changes of state.