Antiprenexing for WSkS: A Little Goes a Long Way

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F20%3APU138621" target="_blank" >RIV/00216305:26230/20:PU138621 - isvavai.cz</a>

Výsledek na webu

<a href="https://www.fit.vut.cz/research/publication/12287/" target="_blank" >https://www.fit.vut.cz/research/publication/12287/</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.29007/6bfc" target="_blank" >10.29007/6bfc</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Antiprenexing for WSkS: A Little Goes a Long Way

Popis výsledku v původním jazyce

We study light-weight techniques for preprocessing of WSkS formulae in an automata-based decision procedure as implemented, e.g., in Mona. The techniques we use are based on antiprenexing, i.e., pushing quantifiers deeper into a formula. Intuitively, this tries to alleviate the explosion in the size of the constructed automata by making it happen sooner on smaller automata (and have the automata minimization reduce the output). The formula transformations that we use to implement antiprenexing may, however, be applied in different ways and extent and, if used in an unsuitable way, may also cause an explosion in the size of the formula and the automata built while deciding it. Therefore, our approach uses informed rules that use an estimation of the cost of constructing automata for WSkS formulae. The estimation is based on a model learnt from runs of the decision algorithm on various formulae. An experimental evaluation of our technique shows that antiprenexing can significantly boost the performance of the base WSkS decision procedure, sometimes allowing one to decide formulae that could not be decided before.

Název v anglickém jazyce

Antiprenexing for WSkS: A Little Goes a Long Way

Popis výsledku anglicky

We study light-weight techniques for preprocessing of WSkS formulae in an automata-based decision procedure as implemented, e.g., in Mona. The techniques we use are based on antiprenexing, i.e., pushing quantifiers deeper into a formula. Intuitively, this tries to alleviate the explosion in the size of the constructed automata by making it happen sooner on smaller automata (and have the automata minimization reduce the output). The formula transformations that we use to implement antiprenexing may, however, be applied in different ways and extent and, if used in an unsuitable way, may also cause an explosion in the size of the formula and the automata built while deciding it. Therefore, our approach uses informed rules that use an estimation of the cost of constructing automata for WSkS formulae. The estimation is based on a model learnt from runs of the decision algorithm on various formulae. An experimental evaluation of our technique shows that antiprenexing can significantly boost the performance of the base WSkS decision procedure, sometimes allowing one to decide formulae that could not be decided before.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2020

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ů

Název statě ve sborníku

EPiC Series in Computing

ISBN

—

ISSN

2398-7340

e-ISSN

—

Počet stran výsledku

19

Strana od-do

298-316

Název nakladatele

EasyChair

Místo vydání

Manchester

Místo konání akce

Alicante

Datum konání akce

23. 5. 2020

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—