×

VPAlib

swMATH ID: 24344
Software Authors: Nguyen H.
Description: 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: Closure operations including union, intersection, and Kleene-star. Determinization : construct a deterministic visibly pushdown automaton from a non-deterministic one. We plan to employ the VPAlib for constructing VPA-based component protocols and then use operations on VPA to analyze properties of those protocols.
Homepage: http://web.imt-atlantique.fr/x-info/hnguyen/vpa/
Related Software: Bebop; OpenNWA; GitHub; Java-MOP; SPIN; BLAST; ALT; XPath
Cited in: 5 Publications

Citations by Year