D 2002

Modifications of Expansion Trees for Weak Bisimulation in BPA

ČERNÁ, Ivana a Jitka STŘÍBRNÁ

Základní údaje

Originální název

Modifications of Expansion Trees for Weak Bisimulation in BPA

Autoři

ČERNÁ, Ivana (203 Česká republika, garant) a Jitka STŘÍBRNÁ (203 Česká republika)

Vydání

The Netherlands, Verification of Infinite-State Systems Infinity'2002, s. 1-21, 2002

Nakladatel

Elsevier Science Publishers

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

20206 Computer hardware and architecture

Stát vydavatele

Nizozemské království

Utajení

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

Kód RIV

RIV/00216224:14330/02:00006476

Organizační jednotka

Fakulta informatiky

ISBN

0444512918

Klíčová slova anglicky

process algebra; weak bisimulation; decidability

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 15:07, prof. RNDr. Ivana Černá, CSc.

Anotace

V originále

The purpose of this work is to examine the decidability problem of weak bisimilarity for BPA-processes. It has been known that strong bisimilarity, which may be considered a special case of weak bisimilarity, where the internal (silent) action $\tau$ is treated equally to observable actions, is decidable for BPA-processes (\cite{BBK,BCS,CHS}). For strong bisimilarity, these processes are finitely branching and so for two non-bisimilar processes there exists a level $n$ that distinguishes the two processes. Additionally, from the decidability of whether two processes are equivalent at a given level $n$, semidecidability of strong non-bisimilarity directly follows. There are two closely related approaches to semidecidability of strong equivalence: construction of a (finite) bisimulation or expansion tree and construction of a finite Caucal base. We have attempted to find out if any of the above mentioned approaches could be generalized to (semi)decide weak bisimilarity.

Návaznosti

GA201/00/0400, projekt VaV
Název: Nekonečně stavové souběžné systémy - modely a verifikace
Investor: Grantová agentura ČR, Nekonečně stavové souběžné systémy - modely a verifikace
GA201/99/D026, projekt VaV
Název: Rozhodnutelnost a složitost observačních ekvivalencí na nekonečně stavových procesech
Investor: Grantová agentura ČR, Rozhodnutelnost a složitost observačních ekvivalencí na nekonečně stavových procesech
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů