Abstract computational model: truncating halt edges, computing reachability and separating halting, stuck and non-terminating runs in a seven-state model

Goal and scope

Given the finite model (S,Init,Step,Halt) with S={s0,s1,s2,s3,s4,s5,s6}, Init={s0}, Halt={s3} and raw edge data {(s0,s1),(s0,s2),(s1,s3),(s1,s5),(s2,s4),(s4,s2),(s3,s6)}: truncate edges out of halt states as the MKO requires, compute the reachable set by fixpoint iteration, identify halt states, stuck states and reachable cycles, exhibit legal halting, stuck and infinite executions, rule out three illegal traces, and explain why depth-bounded exploration that has not exhausted the reachable graph cannot certify termination of all maximal executions merely from the absence of an observed counterexample.

Works inside the MKO's scope: S is an explicitly given finite set of states and Step is a directed relation that may be nondeterministic (assumption a1); reaching Halt stops execution, and edges out of halts are truncated before analysis (assumption a2). Effective encodings, fairness and the layering of deterministic and nondeterministic models are not treated, and the canonical MKO and its English edition are not changed.

Givens and symbols

• set_operations_def
• cartesian_product_def
• subset_def
• nat_induction
• finite_counting_basics

• G1 — S={s0,s1,s2,s3,s4,s5,s6}, Init={s0}, Halt={s3} (MKO assumption a1: S is explicitly finite).
• G2 — Raw edge data E_raw={(s0,s1),(s0,s2),(s1,s3),(s1,s5),(s2,s4),(s4,s2),(s3,s6)}.
• G3 — Execution conventions (MKO assumption a2 and paragraph 2): before analysis, delete every edge leaving a Halt state to obtain Step. An execution is a sequence of states (t_i) indexed by an initial segment of ℕ (finite or all of ℕ), with t_0∈Init and (t_i,t_{i+1})∈Step for consecutive terms; it ends on entering Halt. A finite execution is maximal if its last state has no Step-successor; a finite maximal execution halts if its last state is in Halt and is stuck otherwise; infinite executions are also maximal. Extendible finite prefixes remain legal executions, but not having reached Halt yet does not make such a prefix a counterexample to universal termination. Universal termination below quantifies over maximal executions from Init.

• S — the state set {s0,s1,s2,s3,s4,s5,s6}
• \mathrm{Init},\ \mathrm{Halt} — the initial and halting state sets
• E_{\mathrm{raw}} — the raw edge data
• \mathrm{Step} — the transition relation after truncation
• \mathrm{Post}(s) — the successor set Step[{s}] of s
• R_k — the round-k reachable set (at most k steps)
• \mathrm{Reach} — the set of states reachable from Init

Rules and sources

• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• cartesian_product_def · prerequisite — Cartesian product: A×B is the set of ordered pairs (a,b) with a∈A and b∈B; (a,b)=(c,d) ⇔ a=c and b=d.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_computational_model_def · cited — The finite abstract model in this entry is (S,Init,Step,Halt), with Init,Halt⊆S and Step⊆S×S. Executions start in Init and follow Step; a stuck state without successors is not automatically a member of Halt. · mko-computational-model
• mko_relation_def · cited — A binary relation R from A to B is a subset of A×B; its image of C is R[C]={y∈B: there exists x∈C with (x,y)∈R}. · mko-relation
• reach_def · prerequisite — Reachability: a state s is reachable from Init if there are k≥0 and a finite path of states u_0, u_1 up to u_k with u_0∈Init, u_k=s and every consecutive pair in Step (k=0 means zero steps, i.e. s∈Init). Reach is the set of all reachable states.
• L_fix · lemma — Let R_0=Init and R_{k+1}=R_k∪Step[R_k]. Then (i) for every k, R_k is exactly the set of states reachable in at most k steps; (ii) if R_{m+1}=R_m for some m, then Reach=R_m.

Main derivation

\mathrm{Init}=\{s_0\},\ \mathrm{Halt}=\{s_3\},\ E_{\mathrm{raw}}

\mathrm{Init},\mathrm{Halt}\subseteq S,\ E_{\mathrm{raw}}\subseteq S\times S

E_{\mathrm{raw}}

\mathrm{Step}=E_{\mathrm{raw}}\setminus\{(s_3,s_6)\}=\{(s_0,s_1),(s_0,s_2),(s_1,s_3),(s_1,s_5),(s_2,s_4),(s_4,s_2)\}

\mathrm{Post}(s)=\mathrm{Step}[\{s\}]

\mathrm{Post}:\ s_0\mapsto\{s_1,s_2\},\ s_1\mapsto\{s_3,s_5\},\ s_2\mapsto\{s_4\},\ s_4\mapsto\{s_2\},\ s_3,s_5,s_6\mapsto\varnothing

R_0=\mathrm{Init},\ R_{k+1}=R_k\cup\mathrm{Step}[R_k]

R_{m+1}=R_m\ \Rightarrow\ \mathrm{Reach}=R_m

R_0=\{s_0\}

R_1=\{s_0,s_1,s_2\},\ R_2=\{s_0,s_1,s_2,s_3,s_4,s_5\},\ R_3=R_2\ \Rightarrow\ \mathrm{Reach}=R_2

E_{\mathrm{raw}}[R_2]

s_6\in E_{\mathrm{raw}}[R_2]\ \text{but}\ s_6\notin\mathrm{Reach}

\mathrm{Reach}=\{s_0,s_1,s_2,s_3,s_4,s_5\}

\mathrm{Reach}\cap\mathrm{Halt}=\{s_3\},\ \{s\in\mathrm{Reach}\setminus\mathrm{Halt}\mid\mathrm{Post}(s)=\varnothing\}=\{s_5\}

(s_0,s_1,s_3)

\text{legal execution that halts at}\ s_3

(s_0,s_1,s_5)

\text{legal maximal execution, stuck at}\ s_5\notin\mathrm{Halt}

t_0=s_0,\ t_{2k+1}=s_2,\ t_{2k+2}=s_4\ (k\ge 0)

\forall n\ge 0,\ (t_n,t_{n+1})\in\mathrm{Step},\ t_n\notin\mathrm{Halt}

(s_0,s_3),\ (s_1,s_3),\ (s_0,s_1,s_3,s_6)

\text{none is a legal execution}

\text{stuck execution (S09)},\ \text{infinite execution (S10)}

\neg(\text{every maximal execution from Init halts})

\text{prefixes of depth}\ 1:\ (s_0,s_1),\ (s_0,s_2)

\text{no cycle or stuck state visible at depth 1, yet termination fails}

Substeps and lemmas

R_k

R_k=\{s\mid s\ \text{reachable in at most}\ k\ \text{steps}\}

R_{m+1}=R_m

\forall k\ge m,\ R_k=R_m;\ \mathrm{Reach}=\textstyle\bigcup_k R_k=R_m

Reverse audits

• S13 · premise_audit · S03, S12 — This step rejects inferring termination of all maximal executions merely from the absence of counterexamples in a non-exhaustive depth-bounded observation. It neither rejects complete finite-graph certificates nor claims a general termination decision method for programs.
• S12 · premise_audit · S09, S10, quantifier_negation — Refuting a universal statement needs one counterexample; here there are two of different kinds, matching the two termination risks in MKO paragraph 3.
• S11 · premise_audit · G3, S02, G1 — Each trace is ruled out by naming one violated condition.
• S10 · premise_audit · G3, S02, case_analysis — The case split must cover every n: 0, positive odd, positive even, which are mutually exclusive and exhaustive. The index identity (2k+2)+1=2(k+1)+1 is checked as a degree-one polynomial identity in N5.
• S09 · premise_audit · G3, S02, S07 — Being stuck needs two facts: no successor, and not in Halt.
• S08 · premise_audit · G3, S02 — The three legality conditions are checked one by one. One halting execution does not mean every execution halts (nondeterminism).
• S07 · premise_audit · S03, S05, G1, mko_computational_model_def — The classification uses only the given list Halt and the successor table, never inferring membership in Halt from having no successors.
• S06 · premise_audit · G2, S02, S05 — This step only shows that the result differs with and without truncation, to justify S02; the E_raw result is not taken as a conclusion about the model.
• S05 · premise_audit · S03, L_fix — Each round uses the complete successor table; the stop test is the set equality R_3=R_2 (N3, N4 recompute the sizes).
• S04.2 · premise_audit · S04.1, nat_induction, set_extensionality — The argument needs R_k to be increasing (R_{k+1}⊇R_k by definition) and (i).
• S04.1 · premise_audit · reach_def, nat_induction, set_operations_def, mko_relation_def — Both inclusions are proved in the induction step; the base uses zero-step paths.
• S04 · premise_audit · L_fix, reach_def — The stopping condition must be the set equality R_{m+1}=R_m, not an observation such as 'no new cycle seen in some round'.
• S03 · premise_audit · S02, mko_relation_def — Each of the six edges is assigned to its source exactly once; 2+2+1+1=6 agrees with the edge count (N2).
• S02 · premise_audit · G3, set_operations_def — Each edge's source must be checked against Halt; N1 recomputes the edge count 7−1=6.
• S01 · premise_audit · G1, G2, subset_def, cartesian_product_def — Every element and every edge is checked; this step derives no execution property.

Error controls and negative controls

No outgoing edge does not mean halting

The misconception identified in the MKO is calling a state without outgoing edges a halt automatically. s5 has no successors but is not in Halt, so (s0,s1,s5) is stuck, not halted (S07, S09). Halting is decided only by the given list Halt.

Non-exhaustive finite prefixes do not certify termination

Depth-1 exploration displays neither the cycle s2→s4→s2 nor the stuck s5, yet non-halting maximal executions exist (S12, S13). If the reachable graph has not been exhausted, absence of an observed counterexample is not a termination proof. A complete finite reachable graph permits cycle and non-Halt dead-end checks; general programs still require suitable proof methods.

Truncate edges out of halts first

The raw data contain (s3,s6). Without truncation, s6 would be wrongly counted as reachable and (s0,s1,s3,s6) wrongly accepted as legal (S06, S11). MKO assumption a2 requires deleting such edges before analysis.

• s5 has no successor, so s5 is a halt state → reject — Halt={s3}; s5 is a stuck state, not a halt state.
• Every consecutive pair of (s0,s1,s3,s6) is in the raw data, so it is a legal execution → reject — Execution ends on entering s3∈Halt, and (s3,s6) has been truncated.
• Exploring to depth 1 found no cycle, so every execution terminates → reject — The sequence that leaves s0 and then alternates between s2 and s4 forever is an infinite execution, and (s0,s1,s5) is a stuck execution.
• s6 is reachable because (s3,s6) is in the data → reject — After truncation no edge enters s6, and Reach={s0,s1,s2,s3,s4,s5}.

Result and limitations

After truncation Step has 6 edges; Reach={s0,s1,s2,s3,s4,s5} and s6 is unreachable. s3 is the only reachable halt state, s5 is stuck (no successors but not in Halt), and {s2,s4} is a reachable non-halting cycle. (s0,s1,s3) halts, (s0,s1,s5) is stuck, and the sequence that goes from s0 and then alternates between s2 and s4 forever is an infinite execution; (s0,s3), (s1,s3) and (s0,s1,s3,s6) are illegal. So not every maximal execution from Init halts, and exploration to depth 1 cannot reveal this.

• The layered treatment of deterministic and nondeterministic models, maximal executions, fairness and effective encodings (MKO formal next) is not built here; this guide handles one explicit finite model only.

Verification and source binding

5 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 4e735eff3b7dce6a70f861ddcd8dc409e5a688e22cfd99ecfa7115e5ad0c3ebc
• original source SHA-256: e947537df405a61ccf81d4f1a305ce5e409796bc956b63e5b8517923dab8e201
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)