Computer Science – Formal Languages and Automata Theory
Scientific paper
2009-11-17
EPTCS 10, 2009, pp. 62-76
Computer Science
Formal Languages and Automata Theory
Scientific paper
10.4204/EPTCS.10.5
Visibly pushdown automata (VPA), introduced by Alur and Madhusuan in 2004, is a subclass of pushdown automata whose stack behavior is completely determined by the input symbol according to a fixed partition of the input alphabet. Since its introduce, VPAs have been shown to be useful in various context, e.g., as specification formalism for verification and as automaton model for processing XML streams. Due to high complexity, however, implementation of formal verification based on VPA framework is a challenge. In this paper we consider the problem of implementing VPA-based model checking algorithms. For doing so, we first present an improvement on upper bound for determinization of VPA. Next, we propose simple on-the-fly algorithms to check universality and inclusion problems of this automata class. Then, we implement the proposed algorithms in a prototype tool. Finally, we conduct experiments on randomly generated VPAs. The experimental results show that the proposed algorithms are considerably faster than the standard ones.
No associations
LandOfFree
A Tighter Bound for the Determinization of Visibly Pushdown Automata does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A Tighter Bound for the Determinization of Visibly Pushdown Automata, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Tighter Bound for the Determinization of Visibly Pushdown Automata will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-650564