Visibly Pushdown Automata (VPA), recently introduced by Alur and Madhusudan [1], are special pushdown automata which operate over input alphabets that are partitioned into three disjoint sets of calls, returns and local symbols. The corresponding class of visibly pushdown languages (VPL) has been shown to have many of the desirable properties that regular languages have. VPL is closed under union, intersection, complementation, concatenation and Kleene star. We can also construct a deterministic visibly pushdown automaton from a non-deterministic one.
We have implemented a prototype VPA library (VPAlib) to provide basic operations on VPA to support experimentation of VPA for component protocols. The library has been written using Java 5 and is still under testing and development. The current version VPAlib 0.1 provides the following VPA operations:
The (LGPL-licensed) distribution is available through the following link:
It contains the complete source code, examples for all closure and determinization operations, and an API documentation.