Access Restriction

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

   Open content in new tab
Source: ACM Digital Library