Bisimilarity of Probabilistic Pushdown Automata

FOREJT, Vojtěch, Petr JANČAR, Stefan KIEFER and James WORRELL. Bisimilarity of Probabilistic Pushdown Automata. Online. In Deepak D'Souza and Telikepalli Kavitha and Jaikumar Radhakrishnan. FSTTCS. Dagstuhl: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012, p. 448-460. ISBN 978-3-939897-47-7.

Basic information

• Original name: Bisimilarity of Probabilistic Pushdown Automata
• Authors: FOREJT, Vojtěch (203 Czech Republic, guarantor, belonging to the institution), Petr JANČAR (203 Czech Republic), Stefan KIEFER (276 Germany) and James WORRELL (826 United Kingdom of Great Britain and Northern Ireland).
• Edition: Dagstuhl, FSTTCS, p. 448-460, 13 pp. 2012.
• Publisher: Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik

Other information

• Original language: English
• Type of outcome: Proceedings paper
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• Publication form: electronic version available online
• WWW: URL
• RIV identification code: RIV/00216224:14330/12:00064716
• Organization unit: Faculty of Informatics
• ISBN: 978-3-939897-47-7
• Keywords in English: Bisimulation; infinite state systems; stochastic system

Abstract

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). Our first contribution is a general construction that reduces checking bisimilarity of probabilistic transition systems to checking bisimilarity of non-deterministic transition systems. This construction directly yields decidability of bisimilarity for pPDA, as well as an elementary upper bound for the bisimilarity problem on the subclass of probabilistic basic process algebras, i.e., single-state pPDA. We further show that, with careful analysis, the general reduction can be used to prove an EXPTIME upper bound for bisimilarity of probabilistic visibly pushdown automata. Here we also provide a matching lower bound, establishing EXPTIME-completeness. Finally we prove that deciding bisimilarity of probabilistic one-counter automata, another subclass of pPDA, is PSPACE-complete. Here we use a more specialised argument to obtain optimal complexity bounds.

Links

• LA09016, research and development project: Name: Účast ČR v European Research Consortium for Informatics and Mathematics (ERCIM) (Acronym: ERCIM)

Investor: Ministry of Education, Youth and Sports of the CR, Czech Republic membership in the European Research Consortium for Informatics and Mathematics

• MUNI/33/IP1/2012, interní kód MU: Name: Podpora perspektivních výzkumných týmů Fakulty informatiky a vynikajících vědeckých pracovníků z jiných institucí působících na Fakultě informatiky (Acronym: PVT-VVPZ)

Investor: Masaryk University