A Decision Procedure For The WSkS Logic

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F14%3APU112084" target="_blank" >RIV/00216305:26230/14:PU112084 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

A Decision Procedure For The WSkS Logic

Popis výsledku 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) anddesigns 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.

Název v anglickém jazyce

A Decision Procedure For The WSkS Logic

Popis výsledku anglicky

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) anddesigns 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.

Druh

B - Odborná kniha

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GA14-11384S" target="_blank" >GA14-11384S: Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí</a><br>

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2014

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

978-3-659-63583-0

Počet stran knihy

60

Název nakladatele

Lambert Academic Publishing

Místo vydání

Saarbrücken

Kód UT WoS knihy

—