Detail výsledku

Automata Terms in a Lazy WSkS Decision Procedure

HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Automata Terms in a Lazy WSkS Decision Procedure. In Proceedings of 27th International Conference on Automated Deduction (CADE-27). Lecture Notes in Computer Science. Natal: Springer Verlag, 2019. no. 11716, p. 300-318. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Abstrakt

We propose a lazy decision procedure for the logic WSkS. It builds a term-based symbolic representation of the state space of the tree automaton (TA) constructed by the classical WSkS decision procedure. The classical decision procedure transforms the symbolic representation into a TA via a bottom-up traversal and then tests its language non-emptiness, which corresponds to satisfiability of the formula. On the other hand, we start evaluating the representation from the top, construct the state space on the fly, and utilize opportunities to prune away parts of the state space irrelevant to the language emptiness test. In order to do so, we needed to extend the notion of language terms (denoting language derivatives) used in our previous procedure for the linear fragment of the logic (the so-called WS1S) into automata terms. We implemented our decision procedure and identified classes of formulae on which our prototype implementation is significantly faster than the classical procedure implemented in the Mona tool.

Klíčová slova

WSkS, weak second-order logic, tree automata, lazy evaluation

Rok
2019
Strany
300–318
Časopis
Lecture Notes in Computer Science, roč. 11716, č. 11716, ISSN 0302-9743
Sborník
Proceedings of 27th International Conference on Automated Deduction (CADE-27)
Konference
The 27th International Conference on Automated Deduction
Vydavatel
Springer Verlag
Místo
Natal
DOI
UT WoS
000693450800018
EID Scopus
BibTeX
@inproceedings{BUT159972,
  author="Vojtěch {Havlena} and Lukáš {Holík} and Ondřej {Lengál} and Tomáš {Vojnar}",
  title="Automata Terms in a Lazy WSkS Decision Procedure",
  booktitle="Proceedings of 27th International Conference on Automated Deduction (CADE-27)",
  year="2019",
  journal="Lecture Notes in Computer Science",
  volume="11716",
  number="11716",
  pages="300--318",
  publisher="Springer Verlag",
  address="Natal",
  doi="10.1007/978-3-030-29436-6\{_}18",
  issn="0302-9743",
  url="https://www.fit.vut.cz/research/publication/11973/"
}
Soubory
Projekty
Bezpečné a spolehlivé počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-17-4014, zahájení: 2017-03-01, ukončení: 2020-02-29, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
ROBUST - Verifikace a hledání chyb v pokročilém softwaru, GAČR, Standardní projekty, GA17-12465S, zahájení: 2017-01-01, ukončení: 2019-12-31, ukončen
Výzkumné skupiny
Pracoviště
Nahoru