Refining Undecidability Border of Weak Bisimilarity. (full version of INFINITY 2005 paper)

KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK and Jan STREJČEK. Refining Undecidability Border of Weak Bisimilarity. (full version of INFINITY 2005 paper). Brno: FI MU, 2005. FIMU-RS-2005-06.

Basic information

• Original name: Refining Undecidability Border of Weak Bisimilarity. (full version of INFINITY 2005 paper)
• Name in Czech: Zjemneni hranice nerozhodnutelnosti pro slabou bisimulaci
• Authors: KŘETÍNSKÝ, Mojmír (203 Czech Republic, guarantor), Vojtěch ŘEHÁK (203 Czech Republic) and Jan STREJČEK (203 Czech Republic).
• Edition: Brno, FIMU-RS-2005-06, 2005.
• Publisher: FI MU

Other information

• Original language: English
• Type of outcome: Audiovisual works
• Field of Study: 10201 Computer sciences, information science, bioinformatics
• Country of publisher: Czech Republic
• Confidentiality degree: is not subject to a state or trade secret
• WWW: URL
• RIV identification code: RIV/00216224:14330/05:00012581
• Organization unit: Faculty of Informatics
• Keywords in English: process rewrite systems; state extension; infinite-state; (un)decidability; weak bisimulation
• Tags: (un)decidability, infinite-state, process rewrite systems, state extension, weak bisimulation
• Tags: International impact

Abstract

Weak bisimilarity is one of the most studied behavioural equivalences. This equivalence is undecidable for pushdown processes (PDA), process algebras (PA), and multiset automata (MSA, also known as parallel pushdown processes, PPDA). Its decidability is an open question basic process algebras} (BPA) and basic parallel processes (BPP). We move the undecidability border towards these classes by showing that the equivalence remains undecidable for weakly extended versions of BPA and BPP.

Abstract (in Czech)

Slaba bisimulace je jednou z nejvice studovanych behavioralnich ekvivalenci. Tato ekvivalence je nerozhodnutelna pro pushdown processes (PDA), process algebras (PA), a multiset automata (MSA, zname tez jako parallel pushdown processes, PPDA). Jeji rozhodnutelnost je otevrenym problemem pro question basic process algebras} (BPA) a basic parallel processes (BPP). Ukazujeme, ze hranici jeji nerozhodnutelnosti lze posunout ke zminenym tridam BPA a BPP, a to tak, tato ekvivalence zustava nerohodnutelnou i pro slabe rozsirene verze BPA a BPP.

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

• GD102/05/H050, research and development project: Name: Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů

Investor: Czech Science Foundation, Integrated approach to education of PhD students in the area of parallel and distributed systems

• 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

• 1ET408050503, research and development project: Name: Techniky automatické verifikace a validace softwarových a hardwarových systémů

Investor: Academy of Sciences of the Czech Republic, Techniques for automatic verification and validation of software nad hardware 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