An Alternative Construction in Symbolic Reachability Analysis of Second Order Pushdown Systems

Abstract. Recently, it has been shown that for any higher order pushdown system H and for any regular set C of configurations, the set pre H(C), is regular. In this paper, we give an alternative proof of this result for second order automata. Our construction of automata for recognizing pre H(C) is explicit. The termination of saturation procedure used is obvious. It gives a better bound on size of the automata recognizing pre H(C) if there is no alternation present in H and in the automata recognizing C. Using our techniques for two players reachability games on second order pushdown systems, we generalize some result of [2] concerning synthesis of strategies. Analogous to [2], we show two kinds of winning strategies for player 0 and give algorithms to compute them. The first is executable by second order pushdown automata and the second is linear time executable minimum cost strategy.

• Type: Journal
• Year: 2008
• Where: IJFCS
• Authors: Anil Seth
• Keywords: IJFCS 2008, Order Automata, Order Pushdown, Order Pushdown Systems