Automata Terms in a Lazy WSkS Decision Procedure

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F19%3APU134155" target="_blank" >RIV/00216305:26230/19:PU134155 - isvavai.cz</a>

Výsledek na webu

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

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-29436-6_18" target="_blank" >10.1007/978-3-030-29436-6_18</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Automata Terms in a Lazy WSkS Decision Procedure

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Automata Terms in a Lazy WSkS Decision Procedure

Popis výsledku anglicky

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.

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í

2019

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

Proceedings of 27th International Conference on Automated Deduction (CADE-27)

ISBN

—

ISSN

0302-9743

e-ISSN

—

Počet stran výsledku

19

Strana od-do

300-318

Název nakladatele

Springer Verlag

Místo vydání

Natal

Místo konání akce

Natal

Datum konání akce

22. 8. 2019

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

WRD - Celosvětová akce

Kód UT WoS článku

000693450800018