|
|
Abstraction in Automata Algorithms
Kocourek, Tomáš ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Tato práce si klade za cíl implementaci a experimentální porovnání protiřetězcových algoritmů s abstrakcí a bez abstrakce, které testují prázdnost alternujících automatů. Autor také navrhuje vlastní algoritmy s abstrakcí a navrhuje několik optimalizací pro existující abstraktní algoritmy. Práce popisuje teoretické pozadí studovaných algoritmů a navrhuje efektivní způsob implementace datových struktur, které jsou těmito algoritmy používány. Experimentální vyhodnocení na náhodných automatech ukazuje, že algoritmy bez abstrakce vykazují obecně lepší výsledky, neboť nevyužívají náročné operace průniku a komplementace shora a zdola uzavřených množin. V případě automatů s vysokou hustotou přechodů však algoritmy bez abstrakce zpomalují a algoritmy s abstrakcí naopak zrychlují.
|
|
|
Efficient Algorithms for Finite Automata
Hruška, Martin ; Rogalewicz, Adam (referee) ; Lengál, Ondřej (advisor)
Nondeterministic finite automata are used in many areas of computer science, including, but not limited to, formal verification, the design of digital circuits or for the representation of a regular language. Their advantages over deterministic finite automata is that they may represent a language in even exponentially conciser way. However, this advantage may be lost if a naive approach to some operations is taken, in particular for checking language inclusion of a pair of automata, the naive implementation of which performs an explicit determinization of one of the automata. Recently, several new techniques for this operation that avoid explicit determinization (using the so-called antichains or bisimulation up to congruence) have been proposed. The main goal of the presented work is to efficiently implement these techniques as a new extension of the VATA library. The implementation has been evaluated and is superior to other implementations in over 90% of tested cases by the factor of 2 to 100.
|
|
|
An Efficient Functional Library for Finite Automata
Říha, Jakub ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
Finite automata are an important mathematical abstraction, and in formal verification, they are used for a concise representation of regular languages. Operations often used on finite automata in this setting are testing their universality and language inclusion. \mbox{A naive} approach to implement these operations leads to an explicit determinization of the automata, which can be costly and undesirable. There is, however, a more advanced method for performing those operations, called the Antichains algorithm, which avoids such an explicit determinization. This work shows how finite automata operations can be effectively implemented in Haskell and compares several approaches of their implementation. The obtained results are compared with VATA, an imperative implementation of a finite automata library.
|
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Cílem této práce je vývoj technik umožňujících praktické využití nedeterministických konečných automatů, zejména nedeterministických stromových automatů. Jde zvláště o techniky pro redukci velikosti a testování jazykové inkluze, jež hrají zásadní roli v mnoha oblastech aplikace konečných automatů. V oblasti redukce velikosti vycházíme z dobře známých metod pro slovní automaty které jsou založeny na relacích simulace. Navrhli jsme efektivní algoritmy pro výpočet stromových variant simulačních relací a identifikovali jsme nový typ relace založený na kombinaci takzvaných horních a dolních simulací nad stromovými automaty. Tyto kombinované relace jsou zvláště vhodné pro redukci velikosti automatů slučováním stavů. Navržený princip kombinace relací simulace je relevantní i pro slovní automaty. Náš přínos v oblasti testování jazykové inkluze je dvojí. Nejprve jsme zobecnili na stromové automaty takzvané protiřetězcové algoritmy, které byly původně navrženy pro slovními automaty. Dále se nám podařilo použitím simulačních relací výrazně zefektivnit protiřetězcové algoritmy pro testování jazykové inkluze jak pro slovní, tak pro stromové automaty. Relevanci našich technik pro praxi jsme demonstrovali jejich nasazením v rámci regulárního stromového model checkingu, což je verifikační metoda založená na stromových automatech. Použití našich algoritmů zde vedlo k výraznému zrychlení a zvětšení škálovatelnosti celé metody. Základní myšlenky našich algoritmů pro redukci velikosti automatů a testování jazykové inkluze jsou aplikovatelné i na jiné typy automatů. Příkladem jsou naše redukční techniky pro alternující Büchiho automaty prezentované v poslední části práce.
|
|
|
Efficient Algorithms for Finite Automata
Kantor, Tomáš ; Rogalewicz, Adam (referee) ; Lengál, Ondřej (advisor)
This thesis presents new algorithm for complement of nondeterministic finite automata. State-of-the-art methods require conversion to deterministic finite automata, which can have exponentially larger number of states. This new algorithm works separately on each strongly connected component of finite automata. This approach allows to create complement of each component, reduce it and combine with other parts. This algorithm was proven to create less states for specific types of finite automata than existing methods.
|
|
|
Abstraction in Automata Algorithms
Kocourek, Tomáš ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Tato práce si klade za cíl implementaci a experimentální porovnání protiřetězcových algoritmů s abstrakcí a bez abstrakce, které testují prázdnost alternujících automatů. Autor také navrhuje vlastní algoritmy s abstrakcí a navrhuje několik optimalizací pro existující abstraktní algoritmy. Práce popisuje teoretické pozadí studovaných algoritmů a navrhuje efektivní způsob implementace datových struktur, které jsou těmito algoritmy používány. Experimentální vyhodnocení na náhodných automatech ukazuje, že algoritmy bez abstrakce vykazují obecně lepší výsledky, neboť nevyužívají náročné operace průniku a komplementace shora a zdola uzavřených množin. V případě automatů s vysokou hustotou přechodů však algoritmy bez abstrakce zpomalují a algoritmy s abstrakcí naopak zrychlují.
|
|
|
Efficient Algorithms for Finite Automata
Kantor, Tomáš ; Rogalewicz, Adam (referee) ; Lengál, Ondřej (advisor)
This thesis presents new algorithm for complement of nondeterministic finite automata. State-of-the-art methods require conversion to deterministic finite automata, which can have exponentially larger number of states. This new algorithm works separately on each strongly connected component of finite automata. This approach allows to create complement of each component, reduce it and combine with other parts. This algorithm was proven to create less states for specific types of finite automata than existing methods.
|
|
|
An Efficient Functional Library for Finite Automata
Říha, Jakub ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
Finite automata are an important mathematical abstraction, and in formal verification, they are used for a concise representation of regular languages. Operations often used on finite automata in this setting are testing their universality and language inclusion. \mbox{A naive} approach to implement these operations leads to an explicit determinization of the automata, which can be costly and undesirable. There is, however, a more advanced method for performing those operations, called the Antichains algorithm, which avoids such an explicit determinization. This work shows how finite automata operations can be effectively implemented in Haskell and compares several approaches of their implementation. The obtained results are compared with VATA, an imperative implementation of a finite automata library.
|
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Cílem této práce je vývoj technik umožňujících praktické využití nedeterministických konečných automatů, zejména nedeterministických stromových automatů. Jde zvláště o techniky pro redukci velikosti a testování jazykové inkluze, jež hrají zásadní roli v mnoha oblastech aplikace konečných automatů. V oblasti redukce velikosti vycházíme z dobře známých metod pro slovní automaty které jsou založeny na relacích simulace. Navrhli jsme efektivní algoritmy pro výpočet stromových variant simulačních relací a identifikovali jsme nový typ relace založený na kombinaci takzvaných horních a dolních simulací nad stromovými automaty. Tyto kombinované relace jsou zvláště vhodné pro redukci velikosti automatů slučováním stavů. Navržený princip kombinace relací simulace je relevantní i pro slovní automaty. Náš přínos v oblasti testování jazykové inkluze je dvojí. Nejprve jsme zobecnili na stromové automaty takzvané protiřetězcové algoritmy, které byly původně navrženy pro slovními automaty. Dále se nám podařilo použitím simulačních relací výrazně zefektivnit protiřetězcové algoritmy pro testování jazykové inkluze jak pro slovní, tak pro stromové automaty. Relevanci našich technik pro praxi jsme demonstrovali jejich nasazením v rámci regulárního stromového model checkingu, což je verifikační metoda založená na stromových automatech. Použití našich algoritmů zde vedlo k výraznému zrychlení a zvětšení škálovatelnosti celé metody. Základní myšlenky našich algoritmů pro redukci velikosti automatů a testování jazykové inkluze jsou aplikovatelné i na jiné typy automatů. Příkladem jsou naše redukční techniky pro alternující Büchiho automaty prezentované v poslední části práce.
|
|
|
Efficient Algorithms for Finite Automata
Hruška, Martin ; Rogalewicz, Adam (referee) ; Lengál, Ondřej (advisor)
Nondeterministic finite automata are used in many areas of computer science, including, but not limited to, formal verification, the design of digital circuits or for the representation of a regular language. Their advantages over deterministic finite automata is that they may represent a language in even exponentially conciser way. However, this advantage may be lost if a naive approach to some operations is taken, in particular for checking language inclusion of a pair of automata, the naive implementation of which performs an explicit determinization of one of the automata. Recently, several new techniques for this operation that avoid explicit determinization (using the so-called antichains or bisimulation up to congruence) have been proposed. The main goal of the presented work is to efficiently implement these techniques as a new extension of the VATA library. The implementation has been evaluated and is superior to other implementations in over 90% of tested cases by the factor of 2 to 100.
|
guest ::
