A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F04%3A00010233" target="_blank" >RIV/00216224:14330/04:00010233 - isvavai.cz</a>

Result on the web

—

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata

Original language description

We propose a generic method for deciding semantic equivalences between pushdown automata and finite-state automata. The abstract part of the method is applicable to every process equivalence which is a right PDA congruence. Practical usability of the method is demonstrated on selected equivalences which are conceptual representatives of the whole spectrum. In particular, special attention is devoted to bisimulation-like equivalences (including weak, early, delay, branching, and probabilistic bisimilarity), and it is also shown how the method applies to simulation-like and trace-like equivalences. The generality does not lead to the loss of efficiency; the algorithms obtained by applying our method are essentially time-optimal and sometimes even polynomial. The list of particular results obtained by our method includes items which are first of their kind.

Czech name

Obecná metoda pro automatické rozhodování sémantických ekvivalencí mezi procesy zásobníkových automatů a konečně-stavovými procesy

Czech description

Je podána obecná metoda pro automatické rozhodování sémantických ekvivalencí mezi procesy zásobníkových auomatů a konečně-stavových automatů. Abstraktní část metody je aplikovatelná na libovolnou ekvivalenci, která je pravou PDA kongruencí. Praktická použitelnost metody je demonstrována na vybraných ekvivalencích, které lze označit za konceptuální reprezentanty celého spektra. Zvláštní pozornost je věnována bisimulačním ekvivalencím. Je také ukázáno, jak lze metodu aplikovat na simulační ekvivalence a na ekvivalence podle stop. Obecnost metody nevede ke ztrátě efektivity. Některé ze získaných algoritmů jsou optimální nebo mají dokonce polynomiální složitost.

Type

D - Article in proceedings

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

Z - Vyzkumny zamer (s odkazem do CEZ)

Publication year

2004

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

Exploring New Frontiers of Theoretical Informatics : IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004)

ISBN

1-4020-8140-5

ISSN

—

e-ISSN

—

Number of pages

14

Pages from-to

395-408

Publisher name

Kluwer

Place of publication

Boston, Dordrecht, London

Event location

Toulouse, France

Event date

Aug 22, 2004

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

—