Equivalence Checking of Non-flat Systems Is EXPTIME-hard

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F61989100%3A27240%2F03%3A00008382" target="_blank" >RIV/61989100:27240/03:00008382 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

Equivalence Checking of Non-flat Systems Is EXPTIME-hard

Original language description

The equivalence checking of systems that are given as a composition of interacting finite-state systems is considered. It is shown that the problem is EXPTIME-hard for any notion of equivalence that lies between bisimulation equivalence and trace equivalence, as conjectured by Rabinovich (1997). The result is proved for parallel composition of finite-state systems where hiding of actions is allowed, and for 1-safe Petri nets. The technique of the proof allows to extend this result easily to other typesof `non-flat' systems.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

BD - Information theory

OECD FORD branch

—

Project

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

Continuities

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2003

Confidentiality

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

Article name in the collection

Proceedings of CONCUR 2003 - Concurrency Theory

ISBN

ISBN 3-540-4075

ISSN

—

e-ISSN

—

Number of pages

14

Pages from-to

237-250

Publisher name

Springer-Verlag Berlin Heidelberg

Place of publication

Berlin Heidelberg

Event location

Universite de Provence and Laboratoire d'Informa

Event date

Jan 1, 2003

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—