JANČAR, Petr, Antonín KUČERA a Faron MOLLER. Deciding Bisimilarity between BPA and BPP Processes. Online. R. Amadio, D. Lugiez (Eds.). In Proceedings of 14th International Conference on Concurrency Theory (CONCUR 2003). Berlin: Springer, 2003. s. 159-174. ISBN 3-540-40753-7. [citováno 2024-04-23]
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Deciding Bisimilarity between BPA and BPP Processes
Autoři JANČAR, Petr (203 Česká republika), Antonín KUČERA (203 Česká republika, garant) a Faron MOLLER (124 Kanada)
R. Amadio, D. Lugiez (Eds.).
Vydání Berlin, Proceedings of 14th International Conference on Concurrency Theory (CONCUR 2003), s. 159-174, 2003.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 10201 Computer sciences, information science, bioinformatics
Stát vydavatele Německo
Utajení není předmětem státního či obchodního tajemství
Kód RIV RIV/00216224:14330/03:00008161
Organizační jednotka Fakulta informatiky
ISBN 3-540-40753-7
UT WoS 000185948700010
Klíčová slova anglicky verification; bisimilarity; infinite-state systems
Štítky bisimilarity, infinite-state systems, verification
Příznaky Mezinárodní význam, Recenzováno
Změnil Změnil: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Změněno: 22. 11. 2006 17:28.
Anotace
We identify a necessary condition for when a given BPP process can be expressed as a BPA process. We provide an effective procedure for testing if this condition holds of a given BPP, and in the positive case we provide an effective construction for a particular form of one-counter automaton which is bisimilar to the given BPP. This in turn provides the mechanism to decide bisimilarity between a given BPP process and a given BPA process.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
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: 23. 4. 2024 13:43