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

Kód výsledku v 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>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

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

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2004

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

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

—

Počet stran výsledku

14

Strana od-do

395-408

Název nakladatele

Kluwer

Místo vydání

Boston, Dordrecht, London

Místo konání akce

Toulouse, France

Datum konání akce

22. 8. 2004

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

WRD - Celosvětová akce

Kód UT WoS článku

—