1

From the following definitions:

Definition (Büchi Pushdown System) A Buchi pushdown system (BPDS) is a tuple BP = (Q,S,→,Qf) with (Q,S,→) a PDS (where S is the stack content) and Qf ⊆ Q a set of final states.

The semantics is defined in terms of infinite runs r = (q0,w0) → (q1,w1) → ... A run is accepting if qi ∈ Qf for infinitely many configurations (qi ,wi ).

Given a BPDS BP, compute the set C ⊆ CF of all congurations c ∈ C so that BP has an accepting run from c.

Proposition: BP has an accepting run from c ∈ CF if and only if there are configurations (q, ), (qF , u), (q, · v) ∈ CF with qF ∈ QF so that

(1) c →* (q, · w) for some w ∈ S* and

(2) (q, ) →+ (qF , u) →* (q, · v).

I can't understand the conditions above. The automata represent the configuration changes, not the system itself, that's clear. In order to make the automata accept a run we must derivate from c to (q, · v). But I cant undestard the correlation with the second condition.

Some clarification on accepting condition of Büchi Pushdown system is appreciate, as any other references --- since I copied the above definitions from my lecture notes.

Thanks,

Pedro

Pedro Dusso
  • 205

1 Answers1

3

Condition (1) says that BP has a finite run from $c$ to $\langle q,\gamma\cdot w\rangle$ for some $w\in S^*$, where we allow $c$ to be $\langle q,\gamma\cdot w\rangle$. I assume that this means that $\gamma$ is on the top of the stack, and we don’t care what’s below it. Condition (2) now says that there is a finite run of at least one step from here to $\langle q_F,u\cdot w\rangle$ and then a finite run, possibly of zero steps, to $\langle q,\gamma\cdot v\cdot w\rangle$.

More intuitively, (2) says that if we’re in state $q$ with $\gamma$ on the top of stack, there is a non-empty input that takes us to the final state $q_F$ and from there back to state $q$ with $\gamma$ again on the top of the stack. Repeating that input infinitely often will take the machine through $q_F$ infinitely many times, resulting in acceptance of the input $-$ provided that we can get to the configuration $\langle q,\gamma\rangle$ in the first place. Condition (1) just says that we can get from $c$ to $\langle q,\gamma\rangle$, so the two conditions together say that there is at least one accepting run starting at $c$.

Conversely, suppose that BP has an accepting run starting at $c$. $Q_F$ is finite, so there must be some $q_F\in Q_F$ that appears infinitely often in this run. Look at the configurations immediately preceding the occurrences of $q_F$: infinitely many of them must have the same state $q$, and infinitely many of those must have the same symbol $\gamma$ on the top of the stack, since the stack alphabet is finite. Now pick one instance of $\langle q,\gamma\rangle\to\langle q_F,u\rangle$ in this accepting run; the next instance is of the form $\langle q,\gamma\cdot v\rangle\to\langle q_F,w\rangle$ for some $v,w\in S^*$, and we now have the $\langle q,\gamma\rangle$, $\langle q_F,u\rangle$, and $\langle q,\gamma\cdot v\rangle$ required for condition (2).

Brian M. Scott
  • 616,228
  • Wow, perfect answer. Thank you very much! – Pedro Dusso Feb 04 '13 at 08:17
  • @Pedro: You’re very welcome! – Brian M. Scott Feb 04 '13 at 20:45
  • In the converse proof, in the sentence "the next instance is of the form $\langle q,\gamma⋅v \rangle \rightarrow\langle q_F,w\rangle$ for some $v,w∈S^*$", $w = u.v$ right?

    Also, in the converse proof, if $\gamma$ is on the top of the stack, then $u$ has atmost two stack alphabets, but then $\langle q_F, u \rangle \rightarrow^* \langle q,\gamma.v\rangle $ (in the second condition) may not be true?

     – A J Jun 02 '22 at 06:40
  • @AJ: No, we don’t know what $w$ looks like, because we don’t know how the transition affected the stack. I don’t understand your other question, since there is only one stack alphabet, $S$; we don’t really know anything about $u$. – Brian M. Scott Jun 02 '22 at 20:22
  • @BrianM.Scott Thanks for the answer! In the converse proof "Look at the configurations immediately preceding the occurrences of $q_F$" and "infinitely many of those must have the same symbol $\gamma$ on the top of the stack", means that $(q,\gamma)\rightarrow (q_F,u)$ is a transition in $PDA$ right? If so, then since $\gamma$ is a stack symbol, $u$ must be of length atmost $2$ (push operation may add on to $\gamma$) right? – A J Jun 03 '22 at 05:45
  • @AJ: It’s $\langle q,\gamma\rangle\to^+\langle q_F,u\rangle$, not $\langle q,\gamma\rangle\to\langle q_F,u\rangle$, where $\to^+$ represents any finite, non-zero number of transitions, so we really can’t say anything about $u$. (Note also that this implies that $\langle q,\gamma\cdot z\rangle\to^+\langle q_F,u\cdot z\rangle$ for any $z\in S^*$, a fact that is used in the proof.) – Brian M. Scott Jun 03 '22 at 19:04
  • @BrianM.Scott, The converse proof contains the statement "Look at the configurations immediately preceding the occurrences of $q_F$, and infinitely many of those must have the same symbol $\gamma$ on the top of the stack" and "Now pick one instance of $\langle q, \gamma\rangle \rightarrow \langle q_f,u \rangle $ in this accepting run", right? Here $\gamma$ is a stack symbol, right? Therefore $u$ must be of atmost length two, right? I am only asking this in the converse proof! If this is true then in converse proof "$\langle q,\gamma.v \rangle \rightarrow \langle q_f,w\rangle$" means $w = u.v$? – A J Jun 04 '22 at 08:43
  • @AJ: No, that’s not right. In that sentence $\langle q,\gamma\rangle\to\langle q_F,u\rangle$ refers to the specific transition being applied and stands for all possible instances of $\langle q,\gamma\cdot z\rangle\to\langle q_F,u\cdot z\rangle$ for $z\in S^*$. All that matters here is the symbol on the top of the stack; we don’t know and don’t care what’s under it, and that could be different each time. Perhaps I should have written all that out in full, but I thought that it would be clear from context. – Brian M. Scott Jun 04 '22 at 17:58
  • @BrianM.Scott, Thanks for the reply! yes indeed we don't care about what is below the stack! I will write some statements here, please let me know which is incorrect among them, it would be helpful. In the converse proof we have as follows, (1) $\langle q,\gamma \rangle \rightarrow \langle q_F,u \rangle$ is a transition , with $\gamma$ being a stack symbol, right? (2) If statement 1 is true, then $|u|$ is atmost two, right? (3) If statements 1 and 2 are true, then $w=u.v$, right? Note that the above three statements are only concerning the converse proof! – A J Jun 05 '22 at 19:55
  • @AJ: (1) is true; (2) is not, because $u$ can be absolutely any member of $S^$. Similarly, (3) is not, because $w$ can be absolutely any member of $S^$ of the form $z\cdot v$ with $z\in S^*$. – Brian M. Scott Jun 06 '22 at 22:52
  • @BrianM.Scott This is the reasoning used for (2) being correct. Is there a flaw in this reasoning? (statements are numbered with capital alphabets):

    If $\langle q, \gamma \rangle \rightarrow \langle q_F, u \rangle$ is a transition in PDA and $\gamma$ is a stack symbol, then (A) $| \gamma | = 1 $ right? and if so then (B) $|u| \leq 2 $ right? this is so because a transition can either be a push (a stack alphabet), pop (the alphabet $\gamma$), or no stack operation, right?

     – A J Jun 07 '22 at 06:29
  • @AJ: No, that is not right. The transition $\langle q,\gamma\rangle\to\langle q_F,u\rangle$ simply means that if the PDA is in state $q$ with $\gamma$ at the top of the stack, the input character that caused that transition resulted in sending the PDA to state $q_F$, popping the character $\gamma$ off the stack, and pushing the string $u$ onto the stack. Here $u$ can be any member of $S^*$. – Brian M. Scott Jun 07 '22 at 20:53
  • @BrianM.Scott, Thanks for the reply! The converse proof doesn't seem to work on example [![PDA][2]][2]. We get $\langle q, \gamma \rangle = \langle q, \gamma . v \rangle = \langle q_3, a \rangle$ and $\langle q_3, a \rangle \xrightarrow{POP_a} \langle q_f, \epsilon \rangle$, and so $\langle q_f, w \rangle = \langle q_f, \epsilon \rangle$. Right? [2]: https://i.stack.imgur.com/mKSLk.png – A J Jun 08 '22 at 10:26
  • @AJ: I have no idea what you’re trying to do there or how it relates to the theorem, I’m afraid. I don’t even know what your PDA is, since you’ve not specified the input and stack alphabets, and your labels on the transitions in the diagram use a convention with which I’m not familiar. At this point I’m about ready to give up. It’s clear that there’s something that you’re not understanding, but I still can’t tell whether it’s in the structure of the proof, the notation, or something about PDAs in general. – Brian M. Scott Jun 09 '22 at 05:04
  • @BrianM.Scott: unfortunately, there seems to be a bug in the proof! the example https://i.stack.imgur.com/mKSLk.png seems to highlight the bug. We do not need input to conclude whether the PDA has an accepting run, right? The stack symbols are: $S = {a,b}$. $PUSH_{\gamma}$ and $POP_{\gamma}$ represent pushing and popping respectively, symbol $\gamma$. This doesn't matter anyway as the converse proof works on a run, so here is the infinite run (given in the next comment as the character limit for this comment is almost reached!) – A J Jun 09 '22 at 06:42
  • $\rho = \langle q_0, \epsilon \rangle \xrightarrow{PUSH_b} \langle q_1, b \rangle \xrightarrow{PUSH_a} \langle q_2, ab \rangle \xrightarrow{PUSH_a} \langle q_3, aab \rangle \xrightarrow{POP_a} \langle q_f, ab \rangle \xrightarrow{POP_a} \langle q_1, b \rangle \xrightarrow{PUSH_a} \langle q_2, ab \rangle \xrightarrow{PUSH_a} \langle q_3, aab \rangle \xrightarrow{POP_a} \langle q_f, ab \rangle \xrightarrow{POP_a} \cdots$ – A J Jun 09 '22 at 06:45