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 . Here
- is the set of calls (which will lead to push on a stack)
- is the set of returns (which will lead to pop on a stack)
- 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 is a tuple where
- is a finite set of states
- is the set of initial states
- is the set of final states
- is a finite stack alphabet containing a special symbol
Stack always contains as the bottom element. A visibly pushdown automaton never pushes or pops .
Every context-free language is a 'projection' of some visibly pushdown language
Determinization of visibly pushdown automaton
- 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.
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
- Rajeev Alur, P. Madhusudan: Visibly pushdown languages