Detail publikace

Nested Antichains for WS1S

FIEDOR, T. HOLÍK, L. LENGÁL, O. VOJNAR, T.

Originální název

Nested Antichains for WS1S

Typ

článek v časopise ve Web of Science, Jimp

Jazyk

angličtina

Originální abstrakt

We propose a novel approach for coping with alternating quantification as the main source of nonelementary complexity of deciding WS1S formulae. Our approach is applicable within the state-of-the-art automata-based WS1S decision procedure implemented e.g. in Mona. The way in which the standard decision procedure processes quantifiers involves determinization, with its worst case exponential complexity, for every quantifier alternation in the prefix of a formula. Our algorithm avoids building the deterministic automata---instead, it constructs only those of their states needed for (dis)proving validity of the formula. It uses a symbolic representation of the states, which have a deeply nested structure stemming from the repeated implicit subset construction, and prunes the search space by a nested subsumption relation, a generalization of the one used by the so-called antichain algorithms for handling nondeterministic automata. We have obtained encouraging experimental results, in some cases outperforming Mona, and some of the other recently proposed approaches, by several orders of magnitude.

Klíčová slova

antichains WS1S finite automata subsumption

Autoři

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

Vydáno

1. 1. 2019

ISSN

0001-5903

Periodikum

Acta Informatica

Ročník

56

Číslo

3

Stát

Spolková republika Německo

Strany od

205

Strany do

228

Strany počet

24

URL

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

BibTex

@article{BUT161577,
  author="Tomáš {Fiedor} and Lukáš {Holík} and Ondřej {Lengál} and Tomáš {Vojnar}",
  title="Nested Antichains for WS1S",
  journal="Acta Informatica",
  year="2019",
  volume="56",
  number="3",
  pages="205--228",
  doi="10.1007/s00236-018-0331-z",
  issn="0001-5903",
  url="https://www.fit.vut.cz/research/publication/11889/"
}