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

Varování

Publikace nespadá pod Ekonomicko-správní fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

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 MAYR Richard
Rok publikování	2004
Druh	Článek ve sborníku
Konference	Exploring New Frontiers of Theoretical Informatics : IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004)
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
Obor	Informatika
Klíčová slova	Formal verification; Pushdown automata; Semantic equivalences
Popis	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.
Související projekty:	Verifikace nekonečně stavových systémů Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů