Undecidability Results for Bisimilarity on Prefix Rewrite Systems

JANČAR, Petr and Jiří SRBA. Undecidability Results for Bisimilarity on Prefix Rewrite Systems. LNCS, Foundations of Software Science and Computation Structures (FOSSACS'06). Netherlands: Spinger-Verlag, vol. 2006, No 3921, p. 277-291, 2006.

Basic information

• Original name: Undecidability Results for Bisimilarity on Prefix Rewrite Systems
• Name in Czech: Nerozhodnutelnost Bisimulace na Prefixovych Prepisovacich Systemech
• Authors: JANČAR, Petr (203 Czech Republic) and Jiří SRBA (203 Czech Republic, guarantor).
• Edition: LNCS, Foundations of Software Science and Computation Structures (FOSSACS'06), Netherlands, Spinger-Verlag, 2006.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Netherlands
• Confidentiality degree: is not subject to a state or trade secret
• RIV identification code: RIV/00216224:14330/06:00015979
• Organization unit: Faculty of Informatics
• UT WoS: 000237082000019
• Keywords in English: bisimilarity; undecidability; prefix rewriting
• Tags: bisimilarity, prefix rewriting, undecidability
• Tags: International impact, Reviewed

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 Senizergues (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 R -a-> w where R is a regular language) was left open; this was repeatedly indicated by both Stirling and Senizergues. 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 w -a-> R and R1 -a-> R2 and show when they yield low undecidability (Pi^0_1-completeness) and when high undecidability (Sigma^1_1-completeness), all with and without the assumption of normedness.

Abstract (in Czech)

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 Senizergues (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 R -a-> w where R is a regular language) was left open; this was repeatedly indicated by both Stirling and Senizergues. 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 w -a-> R and R1 -a-> R2 and show when they yield low undecidability (Pi^0_1-completeness) and when high undecidability (Sigma^1_1-completeness), all with and without the assumption of normedness.

Links

• GA201/03/1161, research and development project: Name: Verifikace nekonečně stavových systémů

Investor: Czech Science Foundation, Verification of infinite-state systems

• MSM 143300001, plan (intention): Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů

Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing

• MSM0021622419, plan (intention): Name: Vysoce paralelní a distribuované výpočetní systémy

Investor: Ministry of Education, Youth and Sports of the CR, Highly Parallel and Distributed Computing Systems

• 1M0545, research and development project: Name: Institut Teoretické Informatiky

Investor: Ministry of Education, Youth and Sports of the CR, Institute for Theoretical Computer Science