Nested antichains for WS1S

• Published in: Acta informatica 2019-04, Vol.56 (3), p.205-228
• Main Authors: Fiedor, Tomáš, Holík, Lukáš, Lengál, Ondřej, Vojnar, Tomáš
• Format: Article
• Language: English
• Subjects: Algorithms; Complexity; Computer Science; Computer Systems Organization and Communication Networks; Data Structures and Information Theory; Information Systems and Communication Service; Logics and Meanings of Programs; Original Article; Prunes; Software Engineering/Programming and Operating Systems; State of the art; Theory of Computation
• ISSN: 0001-5903; 1432-0525
• DOI: 10.1007/s00236-018-0331-z

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.