Serialisation System

For a selection function $\alpha$, a serialisation state $(F, E)$ transitions to $(F^S, E \cup S)$ for every $S \in \alpha($$\mathsf{is}^{\not\leftarrow}(F)$$,$ $\mathsf{is}^{\not\leftrightarrow}(F)$$,$ $\mathsf{is}^{\leftrightarrow}(F)$$)$, where $F^S$ is the reduct. For a termination function $\beta$, $\mathcal{E}_{\alpha,\beta}(F)$ is the set of all $E$ such that some $(F', E)$ with $\beta(F', E) = 1$ is reachable from $(F, \emptyset)$ in finitely many steps.

Serialisable semantics

The following semantics are serialisable (Thimm, 2022):

The unchallenged semantics is defined via $\alpha_{\mathsf{uc}}$ and $\beta_{\mathsf{uc}}$ (Bengel & Thimm, 2022).