LARA

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

The key restriction compared to nondeterministic pushdown automata is that whether a visibly pushdown automaton will push or pop is determined only by the input symbol. (The automaton can change the state in a non-deterministic way, and can non-deterministically decide what to push.)

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

Every context-free language is a 'projection' of some visibly pushdown language

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 (but we store the call input symbol).

MSOL over strings with matching relation

Thanks to closure properties.

Stack trees

We can associate injectively trees with words over pushdown alphabet, then visibly pushdown languages correspond to regular trees.

Can we obtain closure and other properties from properties of tree automata?

Visibly pushdown grammars

References