With the CTL-deciders proving to be very strong there is the question which machines cannot be proven by it. 10756090 is an example of such a machine. We can proof that there is no regular language that includes all configuration the TM reaches, but rejects all configurations that lead to halting:
Write C(n,m) for (10)^n A0 1^m
Then the TM follows these rules:
- C(n,m) → halt, if n+m odd
- C(n,m) → C(((n+m)/2)+1,n+1), if n+m even
I’ll leave the proof as an exercise for the reader.
We start in C(0,0) and C(n,n) → C(n+1,n+1) for all n, so the machine is infinite and visits C(n,n) for all n.
To see how it behaves with n != m we consider the difference n-m after applying rule 2:
((n+m)/2)+1-(n+1) = (n+m-2n)/2 = -(n-m)/2
So the TM divides the difference of the exponents by 2 (and flips the sign) until the difference becomes odd. Then it halts. This can only go on forever if the difference is 0 to begin with.
Thus C(n,m) → halt, if n!=m
It is impossible for a regular language to separate {C(n,n) for all n} and {C(n,m) for all n!=m}
To finish it off with an argument by savask:
“If there was a regular language containing all non-halting configs of your machine, then we could intersect it with a language (10)* A0 1* and obtain that (10)^n A0 1^n is regular”