ALLpda using computational histories

ALLpda using computational histories

student (guest) 23 Jul 2016 17:20

lecture 10, slide 24:
about the the given solution to make life easier -
after the PDA checks if C1 yields C2, how does it check that C2 yields C3? Doesn't it need to "save" C2 somehow?
It has only one stack, and it can't push C2 into it during the C1->C2 check, but it can't also "go back" to the starting point of C2
after it was read. Where do I wrong?
Maybe we need to define a new valid accepting sequence s.t each configuration repeats itself?

Re: ALLpda using computational histories

Dean Doron 24 Jul 2016 12:21

Yes, your suggestion sounds reasonable.

Re: ALLpda using computational histories

Iftach Haitner 25 Jul 2016 05:39

Alternatively, note that you only need to make sure it is not a configuration history. So you can "guess" non deterministically the index i such that Ci does not yield C_{i+1}