A 2005

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

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

Language

English

Type of outcome

Audiovizuální tvorba

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Czech Republic

Confidentiality degree

není předmětem státního či obchodního tajemství

References:

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

International impact
Změněno: 27/11/2006 15:12, prof. RNDr. Jan Strejček, Ph.D.

Abstract

V originále

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.

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