Büchi Pushdown System Accepting Run

Question

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.

Thanks,

Pedro

Answer 1

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