All

What are you looking for?

All
Projects
Results
Organizations

Quick search

  • Projects supported by TA ČR
  • Excellent projects
  • Projects with the highest public support
  • Current projects

Smart search

  • That is how I find a specific +word
  • That is how I leave the -word out of the results
  • “That is how I can find the whole phrase”

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