Detail publikačního výsledku

Automata Terms in a Lazy WSkS Decision Procedure

HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T.

Originální název

Automata Terms in a Lazy WSkS Decision Procedure

Anglický název

Automata Terms in a Lazy WSkS Decision Procedure

Druh

Článek WoS

Originální 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.

Anglický 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,Tree automata,Automata term,Finite automata,Monadic second-order logic

Klíčová slova v angličtině

WSkS,Tree automata,Automata term,Finite automata,Monadic second-order logic

Autoři

HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T.

Rok RIV

2022

Vydáno

04.08.2021

ISSN

0168-7433

Periodikum

JOURNAL OF AUTOMATED REASONING

Svazek

65

Číslo

7

Stát

Nizozemsko

Strany od

971

Strany do

999

Strany počet

29

URL

https://www.fit.vut.cz/research/publication/12557/

BibTex

@article{BUT175811,
  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",
  journal="JOURNAL OF AUTOMATED REASONING",
  year="2021",
  volume="65",
  number="7",
  pages="971--999",
  doi="10.1007/s10817-021-09597-w",
  issn="0168-7433",
  url="https://www.fit.vut.cz/research/publication/12557/"
}

Dokumenty

Havlena2021_Article_AutomataTermsInALazyWSKSDecisi