On distributed bisimilarity over Basic Parallel Processes

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F05%3A00012177" target="_blank" >RIV/61989100:27240/05:00012177 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

On distributed bisimilarity over Basic Parallel Processes

Popis výsledku v původním jazyce

Distributed bisimilarity is one of non-interleaving equivalences studied on concurrent systems; it refines the classical bisimilarity by taking also the spatial distribution of (sub)components into account. In the area of verification of infinite-state systems, one of the simplest (most basic) classes in the class of Basic Parallel Processes (BPP); here distributed is known to coincide with many other non-interleaving equivalences. While the classical (interleaving) bisimilarity on BPP is known to be PSPACE-complete, for distributed bisimilarity a polynomial time algorithm was shown by Lasota (2003). Lasota's algorithm is technically a bit complicated, and uses the algorithm by Hirshfeld, Jerrum, Moller (1996) for deciding bisimilarity on normed BPP asa subroutine. Lasota has not estimated the degree of the polynomial for his algorithm, and it is not an easy task to do. In this paper we show a direct and conceptually simpler algorithm, which allows to bound the complexity by O(n^3) (w

Název v anglickém jazyce

On distributed bisimilarity over Basic Parallel Processes

Popis výsledku anglicky

Distributed bisimilarity is one of non-interleaving equivalences studied on concurrent systems; it refines the classical bisimilarity by taking also the spatial distribution of (sub)components into account. In the area of verification of infinite-state systems, one of the simplest (most basic) classes in the class of Basic Parallel Processes (BPP); here distributed is known to coincide with many other non-interleaving equivalences. While the classical (interleaving) bisimilarity on BPP is known to be PSPACE-complete, for distributed bisimilarity a polynomial time algorithm was shown by Lasota (2003). Lasota's algorithm is technically a bit complicated, and uses the algorithm by Hirshfeld, Jerrum, Moller (1996) for deciding bisimilarity on normed BPP asa subroutine. Lasota has not estimated the degree of the polynomial for his algorithm, and it is not an easy task to do. In this paper we show a direct and conceptually simpler algorithm, which allows to bound the complexity by O(n^3) (w

Druh

A - Audiovizuální tvorba

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA201%2F03%2F1161" target="_blank" >GA201/03/1161: Verifikace nekonečně stavových systémů</a><br>

Návaznosti

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

Rok uplatnění

2005

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ů

ISBN

—

Místo vydání

Edinburgh

Název nakladatele resp. objednatele

University of Edinburgh

Verze

—

Identifikační číslo nosiče

—