文章基本信息

标题：Game Characterization of Probabilistic Bisimilarity, and Applications to Pushdown Automata
本地全文：下载
作者：Worrell, James ; Kiefer, Stefan ; Jančar, Petr 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2018
卷号：14
期号：4
DOI：10.23638/LMCS-14(4:13)2018
语种：English
出版社：Technical University of Braunschweig
摘要：We study the bisimilarity problem for probabilistic pushdown automata (pPDA)and subclasses thereof. Our definition of pPDA allows both probabilistic andnon-deterministic branching, generalising the classical notion of pushdownautomata (without epsilon-transitions). We first show a generalcharacterization of probabilistic bisimilarity in terms of two-player games,which naturally reduces checking bisimilarity of probabilistic labelledtransition systems to checking bisimilarity of standard (non-deterministic)labelled transition systems. This reduction can be easily implemented in theframework of pPDA, allowing to use known results for standard(non-probabilistic) PDA and their subclasses. A direct use of the reductionincurs an exponential increase of complexity, which does not matter in derivingdecidability of bisimilarity for pPDA due to the non-elementary complexity ofthe problem. In the cases of probabilistic one-counter automata (pOCA), ofprobabilistic visibly pushdown automata (pvPDA), and of probabilistic basicprocess algebras (i.e., single-state pPDA) we show that an implicit use of thereduction can avoid the complexity increase; we thus get PSPACE, EXPTIME, and2-EXPTIME upper bounds, respectively, like for the respective non-probabilisticversions. The bisimilarity problems for OCA and vPDA are known to have matchinglower bounds (thus being PSPACE-complete and EXPTIME-complete, respectively);we show that these lower bounds also hold for fully probabilistic versions thatdo not use non-determinism.
关键词：Computer Science - Logic in Computer Science;Computer Science - Formal Languages and Automata Theory