Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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 fi nal states.

The semantics is defi ned in terms of in finite runs r = (q0,w0) → (q1,w1) → ... A run is accepting if qi ∈ Qf for infi nitely many confi gurations (qi ,wi ).

Given a BPDS BP, compute the set C ⊆ CF of all con gurations 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 con figurations (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.



share|cite|improve this question
up vote 1 down vote accepted

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).

share|cite|improve this answer
Wow, perfect answer. Thank you very much! – Pedro Dusso Feb 4 '13 at 8:17
@Pedro: You’re very welcome! – Brian M. Scott Feb 4 '13 at 20:45

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.