Closed Position Set (CPS) is a decider that @savask reverse engineered from skelet’s code. See The closed position set decider, reverse-engineered from Skelet's program · GitHub for savask’s description.
It is a CTL-like type of decider in the sense that it builds a set of configurations described by a certain abstract language. In the case of CPS, the set it builds is described by:
A) A set of subtapes surrounding the TM head and
B) A graph/network of “continuations” for how each subtape can be extended to the left and to the right. The continuations work on blocks of symbols and say if the block at the edge of your tape is X, then here are a list of blocks {Y, Z, …} that could be added next.
A simple example is:
1RB0RD_1LC1RB_0RA1LD_1LE0LC_1LC1RZ
* Left continuations:
0 -> {0}
1 -> {0, 1}
* Right continuations:
0 -> {0, 1}
1 -> {0, 1}
* Configs:
0 0 A> 0
0 1 B> 0
0 1 B> 1
0 <C 0 1
0 <C 1 1
0 <D 1 0
0 <E 1 1
1 1 B> 0
1 1 B> 1
1 <C 0 1
1 <D 1 0
In this simple case (block size 1 is not common for this proof type) the right side of the tape is unconstrained (either 0 or 1 may come after either 0 or 1) but on the left, once we see a 0, all future symbols will be 0s. Therefore, this language includes all configs: 0^inf 00 <D 10 .*
, but does not contain any .* 10 <D .*
which is the config required to reach halt.