Refining Undecidability Border of Weak Bisimilarity.

KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK and Jan STREJČEK. Refining Undecidability Border of Weak Bisimilarity. BRICS Notes Series. San Francisco, USA, vol. 2005, NS-05-4, p. 3-14. ISSN 0909-3206. 2005.

Basic information

• Original name: Refining Undecidability Border of Weak Bisimilarity.
• 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: BRICS Notes Series, San Francisco, USA, 2005, 0909-3206.

Other information

• Original language: English
• Type of outcome: Article in a journal
• 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:00012580
• 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, Reviewed

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 zasobnikove procesy (PDA), procesove algebry (PA), and multimnozinove automaty (MSA, zname tez jako paralelni zasobnikove procesy, PPDA). Jeji rozhodnutelnost je otevrenym problemem pro zakladni procesove algebry (BPA) a zakladni paralelni procesy (BPP). Ukazujeme, ze hranici jeji nerozhodnutelnosti lze posunout ke zminenym tridam BPA a BPP. Konkretne ukazeme, ze 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

• 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