Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
HAVLENA, V. HOLÍK, L. LENGÁL, O. VALEŠ, O. VOJNAR, T.
Originální název
Antiprenexing for WSkS: A Little Goes a Long Way
Typ
článek ve sborníku ve WoS nebo Scopus
Jazyk
angličtina
Originální abstrakt
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.
Klíčová slova
antiprenexing, automata, preprocessing, weak monadic second-order logic, WSkS
Autoři
HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VALEŠ, O.; VOJNAR, T.
Vydáno
27. 5. 2020
Nakladatel
EasyChair
Místo
Manchester
ISSN
2398-7340
Číslo
73
Strany od
298
Strany do
316
Strany počet
19
URL
https://www.fit.vut.cz/research/publication/12287/
BibTex
@inproceedings{BUT168130, author="Vojtěch {Havlena} and Lukáš {Holík} and Ondřej {Lengál} and Ondřej {Valeš} and Tomáš {Vojnar}", title="Antiprenexing for WSkS: A Little Goes a Long Way", booktitle="EPiC Series in Computing", year="2020", series="Proceedings of LPAR-23", number="73", pages="298--316", publisher="EasyChair", address="Manchester", doi="10.29007/6bfc", issn="2398-7340", url="https://www.fit.vut.cz/research/publication/12287/" }