Complexity of checking bisimilarity between sequential and parallel processes

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F13%3A86088843" target="_blank" >RIV/61989100:27240/13:86088843 - isvavai.cz</a>

Výsledek na webu

<a href="http://link.springer.com/chapter/10.1007%2F978-3-642-40313-2_28" target="_blank" >http://link.springer.com/chapter/10.1007%2F978-3-642-40313-2_28</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-642-40313-2_28" target="_blank" >10.1007/978-3-642-40313-2_28</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Complexity of checking bisimilarity between sequential and parallel processes

Popis výsledku v původním jazyce

Decidability of bisimilarity for Process Algebra (PA) processes, arising by mixing sequential and parallel composition, is a long-standing open problem. The known results for subclasses contain the decidability of bisimilarity between basic sequential (i.e. BPA) processes and basic parallel processes (BPP). Here we revisit this subcase and derive an exponential-time upper bound. Moreover, we show that the problem if a given basic parallel process is inherently sequential, i.e. bisimilar with an unspecified BPA process, is PSPACE-complete. We also introduce a model of one-counter automata, with no zero tests but with counter resets, that capture the behaviour of processes in the intersection of BPA and BPP.

Název v anglickém jazyce

Complexity of checking bisimilarity between sequential and parallel processes

Popis výsledku anglicky

Decidability of bisimilarity for Process Algebra (PA) processes, arising by mixing sequential and parallel composition, is a long-standing open problem. The known results for subclasses contain the decidability of bisimilarity between basic sequential (i.e. BPA) processes and basic parallel processes (BPP). Here we revisit this subcase and derive an exponential-time upper bound. Moreover, we show that the problem if a given basic parallel process is inherently sequential, i.e. bisimilar with an unspecified BPA process, is PSPACE-complete. We also introduce a model of one-counter automata, with no zero tests but with counter resets, that capture the behaviour of processes in the intersection of BPA and BPP.

Druh

D - Stať ve sborníku

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP202%2F11%2F0340" target="_blank" >GAP202/11/0340: Modelování a verifikace paralelních systémů</a><br>

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2013

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ů

Název statě ve sborníku

Lecture Notes in Computer Science. Volume 8087

ISBN

978-3-642-40312-5

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

12

Strana od-do

302-313

Název nakladatele

Springer Verlag

Místo vydání

London

Místo konání akce

Klosterneuburg

Datum konání akce

26. 8. 2013

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—