Timeline for Decidability of inductive invariant existence in Presburger arithmetic
Current License: CC BY-SA 3.0
3 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 16, 2014 at 22:41 | comment | added | Tim | We can use the standard Turing machine reduction to Minsky machines to the naive Presburger encoding. Then every Turing machine state $i$ eventually has a matching Presburger state $i'$ (with $i \leq i'$). The model I had in mind roughly assumes the tape is in binary and there 1 variable for the tape $t$, a variable that is maintained to be the position $2^p$ if the head of M is at position $p$ and uses $2^p$ to split $t$ into 3 variables $\exists l,c,r$ where $l \leq 2^p, c < 2, r \geq 2^{p+1}$ and $(l + p + r = t => c=1)$ or $(l + r = t => c=0)$. Hope the rest of the encoding is clear. | |
| Apr 16, 2014 at 19:35 | comment | added | cody | This is great, thanks! Do you have a reference for step 2, namely the "compiler from TM to Presburger Arithmetic"? That seems to be the crux of the proof. | |
| Apr 15, 2014 at 22:53 | history | answered | Tim | CC BY-SA 3.0 |