On model checking for visibly pushdown automata

In this paper we improve our previous work by introducing optimized on-the-fly algorithms to test universality and inclusion problems of visibly pushdown automata. We implement the proposed algorithms in a prototype tool. We conduct experiments on randomly generated VPA. The experimental results show that the proposed method outperforms the standard one by several orders of magnitude.