Regularity in Model Checking PDA Games
Václav Brožek · 2007
Abstract. Concerning the model-checking problem of 1 1 2-player games over transition graphs of pushdown automata (PDA) against the reach-ability objectives, we investigate the regularity of sets of configurations satisfying a given reachability objective. This is a natural question con-nected, e.g., to decidability of PCTL model checking. It was shown that these sets may not be regular even for probabilistic stateless pushdown automata (pBPA). We prove, however, that restriction to qualitative reachability objective renders these sets regular for all 1 1 2-player PDA games. As a completion of the answer to the regularity question, we also prove that for quantitative termination objective and 2 1 2-player games over stateless PDA (BPA) the sets of configurations satisfying the ter-mination property are always regular. 1