Visibly Pushdown Automata Library

Overview

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:

We plan to employ the VPAlib for constructing VPA-based component protocols and then use operations on VPA to analyze properties of those protocols.

Download

The (LGPL-licensed) distribution is available through the following link:

VPAlib-0_1.tar.gz (07 Feb. 2006)

It contains the complete source code, examples for all closure and determinization operations, and an API documentation.

References

[1] Rajeev Alur and Parthasarathy Madhusudan. Visibly pushdown languages. In Proceedings of the thirty-sixth annual ACM Symposium on Theory of Computing (STOC-04), pages 202-211, New York, June 13-15 2004. ACM Press.


last update on 07 Feb. 2006 by Ha Nguyen