9 - Pushdown systems

Question 1

translate a problem to pds

Answer 1

We want to check if P |= φ ∈ LTL

Global model checking: Compute the set C ⊆ CF of all configurations c ∈ C so that every run starting from c satisfies φ.

P-NFA A accepts configuration (q,w) of pushdown system PDS P if A accepts w

P-NFA A represents the set of configurations of PDS P

Problem is reduced to reachability (that 2 sentences that uses pre)

Question 2

know corresponding automata of a pds

Answer 2

P-NFA, creates the configurations accepted by PDS

Question 3

pds represent recursive programs

Answer 3

because of stack and stuff

Question 4

runtime states of pds, decide reachability, why is it computable problem?

Answer 4

BPDS BP accepts c ∈ CF iff
- 2 sentences that can be calculated in polynomial time are true

both sentences uses pre* and pre+, thats why pre calculation is important

Question 5

Accepting run problem?

Answer 5

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

Question 6

Global model checking problem?

Answer 6

Compute the set C ⊆ CF of all congurations c ∈ C

so that every run starting from c satises φ.