BRÁZDIL, Tomáš, Antonín KUČERA a Oldřich STRAŽOVSKÝ. Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems. P. Gardner, N. Yoshida (Eds.). In Proceedings of 15th International Conference on Concurrency Theory (CONCUR 2004). Berlin: Springer, 2004. s. 193-208, 16 s. ISBN 3-540-22940-X.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems
Název česky Rozhodnutelnost pravděpodobnostní bisimulace pro nekonečně-stavové pravděpodobnostní systémy
Autoři BRÁZDIL, Tomáš (203 Česká republika), Antonín KUČERA (203 Česká republika, garant) a Oldřich STRAŽOVSKÝ (203 Česká republika).
P. Gardner, N. Yoshida (Eds.).
Vydání Berlin, Proceedings of 15th International Conference on Concurrency Theory (CONCUR 2004), od s. 193-208, 16 s. 2004.
Nakladatel Springer
Další údaje
Originální jazyk angličtina
Typ výsledku Stať ve sborníku
Obor 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/04:00010251
Organizační jednotka Fakulta informatiky
ISBN 3-540-22940-X
UT WoS 000223795700013
Klíčová slova anglicky probabilistic bisimilarity; probabilistic systems
Štítky probabilistic bisimilarity, probabilistic systems
Změnil Změnil: doc. RNDr. Tomáš Brázdil, Ph.D., učo 4074. Změněno: 4. 2. 2005 15:02.
Anotace
We prove that probabilistic bisimilarity is decidable over probabilistic extensions of BPA and BPP processes. For normed subclasses of probabilistic BPA and BPP processes we obtain polynomial-time algorithms. Further, we show that probabilistic bisimilarity between probabilistic pushdown automata and finite-state systems is decidable in exponential time. If the number of control states in PDA is bounded by a fixed constant, then the algorithm needs only polynomial time.
Anotace česky
V článku je dokázáno, že pravděpodobnostní bisimulace je rozhodnutelná pro pravděpodobnostní rozšíření BPA a BPP procesů. Pro normované podtřídy pravděpodobnostních BPA a BPP procesů jsou prezentovány algoritmy, jejichž časová složitost je polynomiální. Dále je dokázáno, že pravděpodobnostní bisimulace mezi pravděpodobnostními zásobníkovými automaty a konečně-stavovými pravděpodobnostními systémy je rozhodnutelná v exponenciálním čase. Pokud je počet kontrolních stavů zásobníkového automatu omezen fixní konstantou, pak je tato časová složitost polynomiální.
Návaznosti
GA201/03/1161, projekt VaVNázev: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Standardní projekty
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, Výzkumné záměry
VytisknoutZobrazeno: 23. 10. 2019 23:59