J 2005

Refining Undecidability Border of Weak Bisimilarity.

KŘETÍNSKÝ, Mojmír, Vojtěch ŘEHÁK a Jan STREJČEK

Základní údaje

Originální název

Refining Undecidability Border of Weak Bisimilarity.

Název česky

Zjemneni hranice nerozhodnutelnosti pro slabou bisimulaci

Autoři

KŘETÍNSKÝ, Mojmír (203 Česká republika, garant), Vojtěch ŘEHÁK (203 Česká republika) a Jan STREJČEK (203 Česká republika)

Vydání

BRICS Notes Series, San Francisco, USA, 2005, 0909-3206

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

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

Odkazy

Kód RIV

RIV/00216224:14330/05:00012580

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

process rewrite systems; state extension; infinite-state; (un)decidability; weak bisimulation

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 4. 12. 2006 16:38, prof. RNDr. Mojmír Křetínský, CSc.

Anotace

ORIG CZ

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.

Česky

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.

Návaznosti

GA201/03/1161, projekt VaV
Název: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM0021622419, záměr
Název: Vysoce paralelní a distribuované výpočetní systémy
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Vysoce paralelní a distribuované výpočetní systémy
1ET408050503, projekt VaV
Název: Techniky automatické verifikace a validace softwarových a hardwarových systémů
Investor: Akademie věd ČR, Techniky automatické verifikace a validace softwarových a hardwarových systémů
1M0545, projekt VaV
Název: Institut Teoretické Informatiky
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Institut Teoretické Informatiky