Abstract:
We answer an open question related to bisimilarity checking on
labelled transition systems generated by prefix rewrite rules on words.
Stirling (1996, 1998) proved the decidability of bisimilarity for normed
pushdown processes. This result was substantially extended by Sénizergues
(1998, 2005) who showed the decidability for regular (or equational) graphs
of finite out-degree (which include unnormed pushdown processes). The
question of decidability of bisimilarity for a more general class of so
called Type -1 systems (generated by prefix rewrite rules of the form
where 
is a regular language) was left
open; this was repeatedly indicated by both Stirling and Sénizergues.
Here we answer the question negatively, i.e., we show undecidability of
bisimilarity on Type -1 systems, even in the normed case. We complete the
picture by considering classes of systems that use rewrite rules of the form
and
and show when they yield low undecidability (
-completeness) and
when high undecidability (
-completeness), all with and without
the assumption of normedness.
where is a regular language) was left
open; this was repeatedly indicated by both Stirling and Sénizergues.
Here we answer the question negatively, i.e., we show undecidability of
bisimilarity on Type -1 systems, even in the normed case. We complete the
picture by considering classes of systems that use rewrite rules of the form
and
and show when they yield low undecidability (-completeness) and
when high undecidability (-completeness), all with and without
the assumption of normedness.Available as PostScript, PDF, DVI.