Další formáty:
BibTeX
LaTeX
RIS
@article{780198, author = {Jančar, Petr and Srba, Jiří}, article_location = {New York}, article_number = {1}, keywords = {undecidability; bisimilarity; rewrite systems}, language = {eng}, issn = {00045411}, journal = {Journal of the ACM}, title = {Undecidability of Bisimilarity by Defender's Forcing}, volume = {55/2008}, year = {2008} }
TY  JOUR ID  780198 AU  Jančar, Petr  Srba, Jiří PY  2008 TI  Undecidability of Bisimilarity by Defender's Forcing JF  Journal of the ACM VL  55/2008 IS  1 SP  126 EP  126 PB  ACM SN  00045411 KW  undecidability KW  bisimilarity KW  rewrite systems N2  tirling (1996, 1998) proved the decidability of bisimilarity on socalled normed pushdown processes. This result was substantially extended by Senizergues(1998, 2005) who showed the decidability of bisimilarity for regular (or equational) graphs of finite outdegree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where the epsilontransitions 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 epsilonpopping pushdown processes, was left open. This was repeatedly indicated by both Stirling and Senizergues. 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 Pi^0_1complete or Sigma^1_1complete. Second, we solve the decidability question for weak bisimilarity on PA (Process Algebra) processes, showing that the problem is undecidable and even Sigma^1_1complete. Third, we show Sigma^1_1completeness of weak bisimilarity for socalled parallel pushdown (or multiset) automata, a subclass of (labeled, place/transition) Petri nets. ER 
JANČAR, Petr a Jiří SRBA. \textit{Undecidability of Bisimilarity by Defender's Forcing}. \textit{Journal of the ACM}, New York: ACM, 2008, roč.~55/2008, č.~1, s.~126. ISSN~00045411.
