Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata
| Autor: | Forejt, V, Jancar, P, Kiefer, S, Worrell, J |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Logic in Computer Science TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES TheoryofComputation_COMPUTATIONBYABSTRACTDEVICES Formal Languages and Automata Theory (cs.FL) TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Computer Science - Formal Languages and Automata Theory Computer Science::Formal Languages and Automata Theory Logic in Computer Science (cs.LO) |
| ISSN: | 1860-5974 |
| DOI: | 10.23638/lmcs-14(4:13)2018 |
| Popis: | We study the bisimilarity problem for probabilistic pushdown automata (pPDA) and subclasses thereof. Our definition of pPDA allows both probabilistic and non-deterministic branching, generalising the classical notion of pushdown automata (without epsilon-transitions). We first show a general characterization of probabilistic bisimilarity in terms of two-player games, which naturally reduces checking bisimilarity of probabilistic labelled transition systems to checking bisimilarity of standard (non-deterministic) labelled transition systems. This reduction can be easily implemented in the framework of pPDA, allowing to use known results for standard (non-probabilistic) PDA and their subclasses. A direct use of the reduction incurs an exponential increase of complexity, which does not matter in deriving decidability of bisimilarity for pPDA due to the non-elementary complexity of the problem. In the cases of probabilistic one-counter automata (pOCA), of probabilistic visibly pushdown automata (pvPDA), and of probabilistic basic process algebras (i.e., single-state pPDA) we show that an implicit use of the reduction can avoid the complexity increase; we thus get PSPACE, EXPTIME, and 2-EXPTIME upper bounds, respectively, like for the respective non-probabilistic versions. The bisimilarity problems for OCA and vPDA are known to have matching lower bounds (thus being PSPACE-complete and EXPTIME-complete, respectively); we show that these lower bounds also hold for fully probabilistic versions that do not use non-determinism. Logical Methods in Computer Science ; Volume 14, Issue 4 ; 1860-5974 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|