KUČERA, Antonín and Richard MAYR. A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata. In Exploring New Frontiers of Theoretical Informatics : IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004). Boston, Dordrecht, London: Kluwer. p. 395-408. ISBN 1-4020-8140-5. 2004.
Other formats:   BibTeX LaTeX RIS
Basic information
Original name A Generic Framework for Checking Semantic Equivalences between Pushdown Automata and Finite-State Automata
Name in Czech Obecná metoda pro automatické rozhodování sémantických ekvivalencí mezi procesy zásobníkových automatů a konečně-stavovými procesy
Authors KUČERA, Antonín (203 Czech Republic, guarantor) and Richard MAYR (276 Germany).
Edition Boston, Dordrecht, London, Exploring New Frontiers of Theoretical Informatics : IFIP 18th World Computer Congress, TC1 3rd International Conference on Theoretical Computer Science (TCS2004), p. 395-408, 14 pp. 2004.
Publisher Kluwer
Other information
Original language English
Type of outcome Proceedings paper
Field of Study 10201 Computer sciences, information science, bioinformatics
Country of publisher United States of America
Confidentiality degree is not subject to a state or trade secret
RIV identification code RIV/00216224:14330/04:00010233
Organization unit Faculty of Informatics
ISBN 1-4020-8140-5
UT WoS 000227054700031
Keywords in English Formal verification; Pushdown automata; Semantic equivalences
Tags formal verification, pushdown automata, semantic equivalences
Tags International impact, Reviewed
Changed by Changed by: prof. RNDr. Antonín Kučera, Ph.D., učo 2508. Changed: 22/11/2006 17:28.
Abstract
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.
Abstract (in Czech)
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.
Links
GA201/03/1161, research and development projectName: Verifikace nekonečně stavových systémů
Investor: Czech Science Foundation, Verification of infinite-state systems
MSM 143300001, plan (intention)Name: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů
Investor: Ministry of Education, Youth and Sports of the CR, Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing
PrintDisplayed: 28/3/2024 16:30