Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete

Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F03%3A00008368" target="_blank" >RIV/61989100:27240/03:00008368 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—

Jazyk výsledku
angličtina
Název v původním jazyce
Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete
Popis výsledku v původním jazyce
The paper shows an algorithm which, given a Basic Parallel Processes (BPP) system, constructs a set of linear mappings which characterize the (strong) bisimulation equivalence on the system. Though the number of the constructed mappings can be exponential, they can be generated in polynomial space; this shows that the problem of deciding bisimulation equivalence on BPP is in PSPACE. Combining with the PSPACE-hardness result by Srba, PSPACE-completeness is thus established.
Název v anglickém jazyce
Strong Bisimilarity on Basic Parallel Processes is PSPACE-complete
Popis výsledku anglicky
The paper shows an algorithm which, given a Basic Parallel Processes (BPP) system, constructs a set of linear mappings which characterize the (strong) bisimulation equivalence on the system. Though the number of the constructed mappings can be exponential, they can be generated in polynomial space; this shows that the problem of deciding bisimulation equivalence on BPP is in PSPACE. Combining with the PSPACE-hardness result by Srba, PSPACE-completeness is thus established.

Projekt
<a href="/cs/project/GA201%2F03%2F1161" target="_blank" >GA201/03/1161: Verifikace nekonečně stavových systémů</a><br>
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění
2003
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Podobné výsledky(10)