AN ALTERNATIVE CONSTRUCTION IN SYMBOLIC REACHABILITY ANALYSIS OF SECOND ORDER PUSHDOWN SYSTEMS
Anil Seth · International Journal of Foundations of Computer Science · 2008
Recently, it has been shown that for any higher order pushdown system [Formula: see text] and for any regular set [Formula: see text] of configurations, the set [Formula: see text], is regular. In this paper, we give an alternative proof of this result for second order automata. Our construction of automaton for recognizing [Formula: see text] is explicit. The termination of saturation procedure used is obvious. It gives EXPTIME bound on size of the automaton recognizing [Formula: see text] if there is no alternation present in [Formula: see text] and in the automaton recognizing [Formula: see text].