Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F18%3A10241459" target="_blank" >RIV/61989100:27240/18:10241459 - isvavai.cz</a>
Alternative codes found
RIV/61989592:15310/18:73590198
Result on the web
<a href="https://lmcs.episciences.org/4972/pdf" target="_blank" >https://lmcs.episciences.org/4972/pdf</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.23638/LMCS-14(4:13)2018" target="_blank" >10.23638/LMCS-14(4:13)2018</a>
Alternative languages
Result language
angličtina
Original language name
Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata
Original language description
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.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
<a href="/en/project/GA15-13784S" target="_blank" >GA15-13784S: Computational complexity of selected verification problems</a><br>
Continuities
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Others
Publication year
2018
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Logical Methods in Computer Science
ISSN
1860-5974
e-ISSN
—
Volume of the periodical
14
Issue of the periodical within the volume
4:13
Country of publishing house
DE - GERMANY
Number of pages
25
Pages from-to
1-25
UT code for WoS article
000452745300017
EID of the result in the Scopus database
2-s2.0-85060234395