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