TY - JOUR

T1 - Undecidability of Bisimilarity by Defender's Forcing

AU - Jancar, Petr

AU - Srba, Jiri

PY - 2008

Y1 - 2008

N2 - Stirling (1996, 1998) proved the decidability of bisimilarity on so called 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 out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where the e-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 e-popping pushdown processes, was left open. This was repeatedly indicated by both Stirling and Senizergues. Here we answer the question negatively, i.e., 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. Firstly, we classify several versions of the undecidable problems for prefix rewrite systems (or pushdown automata) as Pi^0_1-complete or Sigma^1_1-complete. Secondly, we solve the decidability question for weak bisimilarity on PA (Process Algebra) processes, showing that the problem is undecidable and even Sigma^1_1-complete. Thirdly, we show Sigma^1_1-completeness of weak bisimilarity for so called parallel pushdown (or multiset) automata, a subclass of (labelled, place/transition) Petri nets.
Udgivelsesdato: FEB

AB - Stirling (1996, 1998) proved the decidability of bisimilarity on so called 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 out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where the e-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 e-popping pushdown processes, was left open. This was repeatedly indicated by both Stirling and Senizergues. Here we answer the question negatively, i.e., 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. Firstly, we classify several versions of the undecidable problems for prefix rewrite systems (or pushdown automata) as Pi^0_1-complete or Sigma^1_1-complete. Secondly, we solve the decidability question for weak bisimilarity on PA (Process Algebra) processes, showing that the problem is undecidable and even Sigma^1_1-complete. Thirdly, we show Sigma^1_1-completeness of weak bisimilarity for so called parallel pushdown (or multiset) automata, a subclass of (labelled, place/transition) Petri nets.
Udgivelsesdato: FEB

KW - strong and weak bisimilarity

KW - undecidability

KW - arithmetical and analytical hierarchy

KW - process algebra

KW - pushdown automata

KW - Petri nets

KW - PA processes

U2 - 10.1145/1326554.1326559

DO - 10.1145/1326554.1326559

M3 - Journal article

VL - 55

JO - Journal of the Association for Computing Machinery

JF - Journal of the Association for Computing Machinery

SN - 0004-5411

IS - 1

ER -