J 2003

Complexity of Weak Bisimilarity and Regularity for BPA and BPP

SRBA, Jiří

Základní údaje

Originální název

Complexity of Weak Bisimilarity and Regularity for BPA and BPP

Autoři

SRBA, Jiří (203 Česká republika, garant)

Vydání

Mathematical Structures in Computer Science, Great Britain, Cambridge University Press, 2003, 0960-1295

Další údaje

Jazyk

angličtina

Typ výsledku

Článek v odborném periodiku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Velká Británie a Severní Irsko

Utajení

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

Odkazy

Kód RIV

RIV/00216224:14330/03:00008472

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

weak bisimilarity; complexity; process algebra
Změněno: 26. 5. 2004 13:37, Prof. Jiří Srba, Ph.D.

Anotace

V originále

It is an open problem whether weak bisimilarity is decidable for Basic Process Algebra (BPA) and Basic Parallel Processes (BPP). A PSPACE lower bound for BPA and NP lower bound for BPP were demonstrated by Stribrna. Mayr recently achieved a result, saying that weak bisimilarity for BPP is a hard problem for the second level of polynomial hierarchy. We improve this lower bound to PSPACE, moreover for the restricted class of normed BPP. Weak regularity (finiteness) of BPA and BPP is not known to be decidable either. In the case of BPP there is a hardness result for the second level of arithmetical hierarchy by Mayr, which we improve to PSPACE. No lower bound has previously been established for BPA. We demonstrate DP-hardness, which in particular implies both NP and coNP-hardness. In each of the bisimulation/regularity problems we consider also the classes of normed processes. Finally we show how the technique for proving co-NP lower bound for weak bisimilarity of BPA can be applied to strong bisimilarity of BPP.

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ů