RIV/00216305:26230/14:PU112084 - A Decision Procedure For The WSkS Logic
Údaje o výsledku
Identifikační kód:RIV/00216305:26230/14:PU112084 Název v původním jazyce:A Decision Procedure For The WSkS Logic Název česky: Druh:B - Odborná kniha Jazyk:eng - angličtina Obor:IN - Informatika Rok uplatnění:2014 Kód důvěrnosti:S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů Počet tvůrců:1 Počet domácích tvůrců:1 Tvůrce:Fiedor, Tomáš
Údaje blíže specifikující výsledek
Popis v původním jazyce:Various types of logics are often used as a means for formal specification of systems. The weak monadic second-order logic of k successors (WSkS) is one of these logics with quite high expressivity, yet still decidable. Although the complexity of checking satisfiability of a WSkS formula is not even in the ELEMENTARY class, there are approaches to this problem based on deterministic tree automata that perform well in practice, like the MONA tool that efficiently solves the class of practical formulae, but fails for some others. This work extends the class of practically solvable formulae with the use of recently developed techniques for efficient manipulation of non-deterministic automata (such as the antichains algorithm for testing universality) and designs a new decision procedure using non-deterministic automata. The procedure is implemented and is compared with the MONA tool and for some cases yield better results than MONA. Popis česky: Klíčová slova: Název periodka:A Decision Procedure For The WSkS Logic Rozsah stran: ISSN: Svazek periodika: Číslo periodika v rámci uvedeného svazku: Stát vydavatele periodika: Počet stran výsledku:60 DOI:
Údaje o tomto záznamu o výsledku
Předkladatel:Vysoké učení technické v Brně / Fakulta informačních technologií (IČO: 216305) Dodavatel:MSM Rok sběru:2015 Systémové označení dodávky dat:RIV15-MSM-26230___/01:1 Kontrolní kód:[749E2808B757]
