ČERNÁ, Ivana a Jitka STŘÍBRNÁ. Modifications of Expansion Trees for Weak Bisimulation in BPA. In Verification of Infinite-State Systems Infinity'2002. The Netherlands: Elsevier Science Publishers, 2002, s. 1-21. ISBN 0444512918.
Další formáty:   BibTeX LaTeX RIS
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
Originální 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
Štítky decidability, process algebra, weak bisimulation
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnila: prof. RNDr. Ivana Černá, CSc., učo 1419. Změněno: 22. 11. 2006 15:07.
Anotace
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 VaVNá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 VaVNá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ěrNá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ů
VytisknoutZobrazeno: 4. 5. 2024 05:54