Name
Title | ||
|---|---|---|
Deciding probabilistic simulation between probabilistic pushdown automata and finite-state systems. |
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2019 | 10.1016/j.ic.2019.05.004 | Information and Computation |
Keywords | DocType | Volume |
Probabilistic pushdown automata,Simulation preorder,Infinite-state systems | Journal | 268 |
ISSN | Citations | PageRank |
0890-5401 | 1 | 0.35 |
References | Authors | |
0 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Mingzhang Huang | 1 | 1 | 0.35 |
| Hongfei Fu | 2 | 87 | 8.32 |
| Joost-Pieter Katoen | 3 | 4444 | 289.65 |