Nested antichains for WS1S

DOI10.1007/S00236-018-0331-ZMaRDI QIDQ1733101zbMATH OpenOpenAlexFDO

Authors Tomáš Fiedor, Lukáš Holik, Ondřej Lengál, Tomáš Vojnar

Publication date 21 March 2019

Published in Acta Informatica (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1501.03849

Mathematics Subject Classification ID

Automata and formal grammars in connection with logical questions (03D05) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

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 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 by several orders of magnitude.

Recommendations

• Nested antichains for WS1S
• Lazy automata techniques for WS1S
• MONA IMPLEMENTATION SECRETS
• scientific article; zbMATH DE number 1773084
• scientific article; zbMATH DE number 1841832

Cites work

• scientific article; zbMATH DE number 1614700 (Why is no real title available?)
• scientific article; zbMATH DE number 3510287 (Why is no real title available?)
• scientific article; zbMATH DE number 3229502 (Why is no real title available?)
• A coalgebraic decision procedure for WS1S
• An efficient decision procedure for imperative tree data structures
• Antichain algorithms for finite automata
• Antichain-Based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata
• Antichains: A New Algorithm for Checking Universality of Finite Automata
• Array theory of bounded elements and its applications
• Automated verification of shape, size and bag properties via user-defined predicates in separation logic
• Computing Simulations over Tree Automata
• Decidable logics combining heap structures and data
• Forest automata for verification of heap manipulation
• MONA IMPLEMENTATION SECRETS
• Minimization of symbolic automata
• Nested antichains for WS1S
• New algorithm for weak monadic second-order logic on inductive structures
• The tree width of separation logic with recursive definitions
• VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata
• When simulation meets antichains. (On checking language inclusion of nondeterministic finite (tree) automata)

Cited in

(5)

• Lazy automata techniques for WS1S
• Nested antichains for WS1S
• MONA IMPLEMENTATION SECRETS
• scientific article; zbMATH DE number 1773084 (Why is no real title available?)
• Language inclusion algorithms as complete abstract interpretations

Describes a project that uses

Uses Software

• Slide
• Antichains
• MTBDD
• VATA
• HIP
• MONA

This page was built for publication: Nested antichains for WS1S

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1733101)