Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems

Checking whether a pushdown automaton is simulated - in the sense of a simulation pre-order - by a finite-state automaton is EXPTIME-complete. This paper shows that the same computational complexity is obtained in a probabilistic setting. That is, the problem of deciding whether a probabilistic pushdown automaton (pPDA) is simulated by a finite Markov decision process (MDP) is EXPTIME-complete. The considered pPDA contain both probabilistic and non-deterministic branching. The EXPTIME-membership is shown by combining a partition-refinement algorithm with a tableaux system that is inspired by Stirling's technique for bisimilarity checking of ordinary pushdown automata. The hardness is obtained by exploiting the EXPTIME-hardness for the non-probabilistic case. Moreover, our decision problem is in PTIME when both the number of states of the pPDA and the number of states in the MDP are fixed. (C) 2019 Elsevier Inc. All rights reserved.