On distributed bisimilarity over Basic Parallel Processes

Result code in 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>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

On distributed bisimilarity over Basic Parallel Processes

Original language description

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

Czech name

On distributed bisimilarity over Basic Parallel Processes

Czech description

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

Type

A - Audiovisual production

CEP classification

IN - Informatics

OECD FORD branch

—

Project

<a href="/en/project/GA201%2F03%2F1161" target="_blank" >GA201/03/1161: Verification of infinite-state systems</a><br>

Continuities

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

Publication year

2005

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

—

Place of publication

Edinburgh

Publisher/client name

University of Edinburgh

Version

—

Carrier ID

—