D 2004

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

KUČERA, Antonín a Richard MAYR

Základní údaje

Originální název

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

Název česky

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

Autoři

KUČERA, Antonín (203 Česká republika, garant) a Richard MAYR (276 Německo)

Vydání

Boston, Dordrecht, London, Exploring New Frontiers of Theoretical Informatics : IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), od s. 395-408, 14 s. 2004

Nakladatel

Kluwer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Spojené státy

Utajení

není předmětem státního či obchodního tajemství

Kód RIV

RIV/00216224:14330/04:00010233

Organizační jednotka

Fakulta informatiky

ISBN

1-4020-8140-5

UT WoS

000227054700031

Klíčová slova anglicky

Formal verification; Pushdown automata; Semantic equivalences

Štítky

Příznaky

Mezinárodní význam, Recenzováno
Změněno: 22. 11. 2006 17:28, prof. RNDr. Antonín Kučera, Ph.D.

Anotace

ORIG CZ

V originále

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.

Česky

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.

Návaznosti

GA201/03/1161, projekt VaV
Název: Verifikace nekonečně stavových systémů
Investor: Grantová agentura ČR, Verifikace nekonečně stavových systémů
MSM 143300001, záměr
Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů