Publication detail

Nested Antichains for WS1S

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

Original Title

Nested Antichains for WS1S

English Title

Nested Antichains for WS1S

Type

conference paper

Language

en

Original Abstract

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 generalisation of the one used by the so-called antichain algorithms for handling non-deterministic automata. We have obtained encouraging experimental results, in some cases outperforming MONA by several orders of magnitude.

English abstract

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 generalisation of the one used by the so-called antichain algorithms for handling non-deterministic automata. We have obtained encouraging experimental results, in some cases outperforming MONA by several orders of magnitude.

Keywords

antichains WS1S finite automata subsumption nondeterministic automata

RIV year

2015

Released

13.04.2015

Publisher

Springer Verlag

Location

Heidelberg

ISBN

978-3-662-46680-3

Book

Proceedings of TACAS'15

Edition

Lecture Notes in Computer Science

Edition number

NEUVEDEN

Pages from

658

Pages to

674

Pages count

17

URL

BibTex


@inproceedings{BUT119806,
  author="Tomáš {Fiedor} and Lukáš {Holík} and Ondřej {Lengál} and Tomáš {Vojnar}",
  title="Nested Antichains for WS1S",
  annote="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 generalisation of the one used by the
so-called antichain algorithms for handling non-deterministic automata. We have
obtained encouraging experimental results, in some cases outperforming MONA by
several orders of magnitude.",
  address="Springer Verlag",
  booktitle="Proceedings of TACAS'15",
  chapter="119806",
  doi="10.1007/978-3-662-46681-0_59",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  year="2015",
  month="april",
  pages="658--674",
  publisher="Springer Verlag",
  type="conference paper"
}