LARA

This is an old revision of the document!

Visibly pushdown languages

What if a property that we wish to check is not regular?

Note that checking inclusion, emptyness of intersection, and universality of context-free languages are all undecidable. So we cannot check (without approximation) whether a pushdown system satisfies a context-free property. This is unfortunate, as some properties are context-free. There is a class of languages that are between regular and context-free and that have good closure properties. These can be used to check some properties that cannot be checked using the first approach.

Visibly pushdown languages are defined with respect to a pushdown alphabet, which is a triple $(\Sigma_c,\Sigma_r,\Sigma_l)$. Here

  • $\Sigma_c$ is the set of calls (which will lead to push on a stack)
  • $\Sigma_r$ is the set of returns (which will lead to pop on a stack)
  • $\Sigma_l$ is the set of local actions (which leave stack the same)

Visibly pushdown automaton

A (nondeterministic) visibly pushdown automaton (on finite words) over the pushdown alphabet $(\Sigma_c,\Sigma_r,\Sigma_l)$ is a tuple $M = (Q,Q_{in},\Gamma,\delta,Q_F)$ where

  • $Q$ is a finite set of states
  • $Q_{in} \subseteq Q$ is the set of initial states
  • $Q_F \subseteq Q$ is the set of final states
  • $\Gamma$ is a finite stack alphabet containing a special symbol $\bot \in \Gamma$
  • $\delta \subseteq \mbox{PushSteps} \cup \mbox{PopSteps} \cup \mbox{LocalSteps}$ where
    • $\mbox{PushSteps} \subseteq Q \times \Sigma_c \times Q \times (\Gamma \setminus\{\bot\})$
    • $\mbox{PopSteps} \subseteq Q \times \Sigma_r \times \Gamma \times Q$
    • $\mbox{LocalSteps} \subseteq Q \times \Sigma_l \times Q$

Stack always contains $\bot$ as the bottom element. A visibly pushdown automaton never pushes or pops $\bot$.

Closure properties

Determinization of visibly pushdown automaton

Note

  • cannot store set of stacks (not a stack)
  • if attempt to store stack of sets of symbols, lose connection between states and stacks

Solution: not just a set of states, but a summary of relation from initial to final states of 'procedure'. Then update directly the effect of a procedure call on each state.

Note: you never store original symbols on the stack.

References