Original title: Rozhodování WS1S pomocí symbolických automatů
Translated title: Deciding WS1S with Automata
Authors: Bednář, Pavel ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
Document type: Master’s theses
Year: 2023
Language: cze
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [cze] [eng]
WS1S je druhořádová logika s jednoduchou syntaxí a sémantikou, nabízející velkou stručnost popisu a rozhodnutelnost pomocí konečných automatů. Bohužel složitost rozhodovací procedůry je nonelementary, což na jednu stranu evokuje problém pro praktické aplikace, ale zároveň to představuje určitý prostor pro různé heuristiky a optimalizace. Nejpoužívanější nástroj v této oblasti, Mona, představuje ukázku toho, že konečné automaty s velkými abecedami mohou pracovat efektivně, a to díky BDD kódování přechodů. V této práci představíme novou rozhodovací procedůru pro WS1S, která zkombinuje klasický přístup s Mona přístupem tak, že přechody reprezentované pomocí BDD integrujeme přímo do automatu. Tím dosáhneme efektivity BDD přechodů, ale zároveň flexiblity díky používání čistě jen automatů a navíc oproti BDD můžeme přeskočit více proměnných nebo pracovat s nedeterminismem. Experimenty ukazují, že jsme schopni v některých oblastech konkurovat nástroji Mona a také dokážeme obecně tvořit automaty s méně stavy než Mona. WS1S is second-order logic with simple syntax and semantics, offering great brevity and decidability using finite automata. Unfortunately, the complexity of the decision procedure is nonelementary, which may sounds like a problem for practical applications, but on the other hand it represents a certain space for various heuristics and optimizations. The most widely used tool in this field, Mona, is a demonstration that finite automata with large alphabets can work efficiently, thanks to BDD encoding of transitions. In this work, we present a novel decision procedure for WS1S that combines the classical approach with the Mona approach by integrating the transitions represented by BDD directly into the automaton. In this way, we achieve the efficiency of BDD transitions, but at the same time flexibility thanks to the use of automata only and in addition, compared to BDD, we can skip more variables or work with non-determinism. Experiments shows that we are able to compete with the Mona in some areas and we are also able to create automata with fewer states than Mona in general.
Keywords: binary decision diagrams; deciding WS1S; finite automata; binární rozhodovací diagramy; konečné automaty; rozhodování WS1S

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/211916

Permalink: http://www.nusl.cz/ntk/nusl-530181


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Master’s theses