D 2004

Deciding Probabilistic Bisimilarity Over Infinite-State Probabilistic Systems

BRÁZDIL, Tomáš, Antonín KUČERA a Oldřich STRAŽOVSKÝ

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

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/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

Změněno: 4. 2. 2005 15:02, doc. RNDr. Tomáš Brázdil, Ph.D.

Anotace

ORIG CZ

V originále

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.

Č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 VaV
Název: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
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ů