Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata

We study the bisimilarity problem for probabilistic pushdown automata (pPDA)and subclasses thereof. Our definition of pPDA allows both probabilistic andnon-deterministic branching, generalising the classical notion of pushdownautomata (without epsilon-transitions). We first show a generalcharacterization of probabilistic bisimilarity in terms of two-player games,which naturally reduces checking bisimilarity of probabilistic labelledtransition systems to checking bisimilarity of standard (non-deterministic)labelled transition systems. This reduction can be easily implemented in theframework of pPDA, allowing to use known results for standard(non-probabilistic) PDA and their subclasses. A direct use of the reductionincurs an exponential increase of complexity, which does not matter in derivingdecidability of bisimilarity for pPDA due to the non-elementary complexity ofthe problem. In the cases of probabilistic one-counter automata (pOCA), ofprobabilistic visibly pushdown automata (pvPDA), and of probabilistic basicprocess algebras (i.e., single-state pPDA) we show that an implicit use of thereduction can avoid the complexity increase; we thus get PSPACE, EXPTIME, and2-EXPTIME upper bounds, respectively, like for the respective non-probabilisticversions. The bisimilarity problems for OCA and vPDA are known to have matchinglower bounds (thus being PSPACE-complete and EXPTIME-complete, respectively);we show that these lower bounds also hold for fully probabilistic versions thatdo not use non-determinism