### Undecidability of bisimilarity by defender's forcingUndecidability of bisimilarity by defender's forcing

Access Restriction
Subscribed

 Author Janar, Petr ♦ Srba, Jiv Source ACM Digital Library Content type Text Publisher Association for Computing Machinery (ACM) File Format PDF Copyright Year ©2008 Language English
 Subject Domain (in DDC) Computer science, information & general works ♦ Data processing & computer science Subject Keyword Bisimilarity ♦ Process algebra ♦ Pushdown automata ♦ Undecidability Abstract Stirling [1996, 1998] proved the decidability of bisimilarity on so-called normed pushdown processes. This result was substantially extended by Sénizergues [1998, 2005] who showed the decidability of bisimilarity for regular (or equational) graphs of finite out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where the $\textit{ϵ}-transitions$ can only deterministically pop the stack. The question of decidability of bisimilarity for the more general class of so called Type -1 systems, which is equivalent to weak bisimilarity on unrestricted $\textit{ϵ}-popping$ pushdown processes, was left open. This was repeatedly indicated by both Stirling and Sénizergues. Here we answer the question negatively, that is, we show the undecidability of bisimilarity on Type -1 systems, even in the normed case. We achieve the result by applying a technique we call Defender's Forcing, referring to the bisimulation games. The idea is simple, yet powerful. We demonstrate its versatility by deriving further results in a uniform way. First, we classify several versions of the undecidable problems for prefix rewrite systems (or pushdown automata) as $Π^{0}_{1}-complete$ or $Σ^{1}_{1}-complete.$ Second, we solve the decidability question for weak bisimilarity on PA (Process Algebra) processes, showing that the problem is undecidable and even $Σ^{1}_{1}-complete.$ Third, we show $Σ^{1}_{1}-completeness$ of weak bisimilarity for so-called parallel pushdown (or multiset) automata, a subclass of (labeled, place/transition) Petri nets. ISSN 00045411 Age Range 18 to 22 years ♦ above 22 year Educational Use Research Education Level UG and PG Learning Resource Type Article Publisher Date 2008-02-01 Publisher Place New York e-ISSN 1557735X Journal Journal of the ACM (JACM) Volume Number 55 Issue Number 1 Page Count 26 Starting Page 1 Ending Page 26

#### Open content in new tab

Source: ACM Digital Library