Nested Antichains for WS1S

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F15%3APU116949" target="_blank" >RIV/00216305:26230/15:PU116949 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-662-46681-0_59" target="_blank" >http://dx.doi.org/10.1007/978-3-662-46681-0_59</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-662-46681-0_59" target="_blank" >10.1007/978-3-662-46681-0_59</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Nested Antichains for WS1S

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Nested Antichains for WS1S

Popis výsledku anglicky

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.

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í

2015

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 TACAS'15

ISBN

978-3-662-46680-3

ISSN

—

e-ISSN

—

Počet stran výsledku

17

Strana od-do

658-674

Název nakladatele

Springer Verlag

Místo vydání

Heidelberg

Místo konání akce

London

Datum konání akce

11. 4. 2015

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

WRD - Celosvětová akce

Kód UT WoS článku

—