Comparing Expressibility of Normed BPA and Normed BPP Processes.

ČERNÁ, Ivana, Mojmír KŘETÍNSKÝ and Antonín KUČERA. Comparing Expressibility of Normed BPA and Normed BPP Processes. Acta informatica. Berlin: Springer-Verlag, 1999, vol. 36, No 3, p. 233-256. ISSN 0001-5903.

Basic information

• Original name: Comparing Expressibility of Normed BPA and Normed BPP Processes.
• Authors: ČERNÁ, Ivana (203 Czech Republic, guarantor), Mojmír KŘETÍNSKÝ (203 Czech Republic) and Antonín KUČERA (203 Czech Republic).
• Edition: Acta informatica, Berlin, Springer-Verlag, 1999, 0001-5903.

Other information

• Original language: English
• Type of outcome: Article in a journal
• Field of Study: 20206 Computer hardware and architecture
• Country of publisher: Germany
• Confidentiality degree: is not subject to a state or trade secret
• Impact factor: Impact factor: 0.321
• RIV identification code: RIV/00216224:14330/99:00000703
• Organization unit: Faculty of Informatics
• UT WoS: 000079817400003
• Keywords in English: concurrency; bisimilarity; infinite-state systems
• Tags: bisimilarity, concurrency, infinite-state systems

Abstract

We present an exact characterization of those transition systems which can be equivalently (up to bisimilarity) defined by the syntax of normed \BPA\ and normed \BPP\ processes. We provide such a characterization for classes of normed BPA and normed BPP processes as well. Next we demonstrate decidability of the problem whether for a given normed \BPA\ process $\Delta$ there is some unspecified normed \BPP\ process $\Delta'$ such that $\Delta$ and $\Delta'$ are bisimilar. The algorithm is polynomial. Furthermore, we show that if the answer to the previous question is positive, then the process $\Delta'$ is effectively constructible. Analogous algorithms are provided for normed \BPP\ processes. Simplified versions of the mentioned algorithms which work for nBPA and nBPP are given too. As a simple consequence we obtain decidability of bisimilarity in the union of normed \BPA\ and normed \BPP\ processes.

Abstract (in Czech)

uvádíme přesnou charakterizaci těch přechodových systémů s návěštími, které lze (až na bisimulačni ekvivalenci) vyjádřit jak pomocí syntaxe normovaných BPA procesů a normovaných BPP procesů. Ukazujeme algoritmickou řešitelnost problému, kdy je dán normovaný BPA proces a jest rozhodnout, zda existuje s ním bisimulačně ekvivaletní normovaný BPP proces. Dále ukazujeme, že pokud odpověď na tento problém ANO, pak lze ekvivaletní BPP proces efektivně zkonstruovat.

Links

• GA201/97/0456, research and development project: Name: Meze algoritmické verifikovatelnosti nekonečně stavových systémů

Investor: Czech Science Foundation, Algorithmic Verification Boundaries for Infinite-State Systems

• GA201/98/P046, research and development project: Name: Rozhodnutelné problémy v algebrách procesů

Investor: Czech Science Foundation, (Un)decidable Problems in Process Algebras

• MSM 143300001, plan (intention): Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů

Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing