Certifying DFA bounds for recognition and separation

DOI10.1007/978-3-030-88885-5_4MaRDI QIDQ2147179zbMATH OpenOpenAlexFDO

Authors Orna Kupferman, Nir Lavee, Salomon Sickert

Publication date 22 June 2022

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

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Applications of game theory (91A80)

Abstract: The automation of decision procedures makes certification essential. We suggest to use determinacy of turn-based two-player games with regular winning conditions in order to generate certificates for the number of states that a deterministic finite automaton (DFA) needs in order to recognize a given language. Given a language $L$ and a bound $k$, recognizability of $L$ by a DFA with $k$ states is reduced to a game between Prover and Refuter. The interaction along the game then serves as a certificate. Certificates generated by Prover are minimal DFAs. Certificates generated by Refuter are faulty attempts to define the required DFA. We compare the length of offline certificates, which are generated with no interaction between Prover and Refuter, and online certificates, which are based on such an interaction, and are thus shorter. We show that our approach is useful also for certification of separability of regular languages by a DFA of a given size. Unlike DFA minimization, which can be solved in polynomial time, separation is NP-complete, and thus the certification approach is essential. In addition, we prove NP-completeness of a strict version of separation.

Recommendations

• Learning Minimal Separating DFA’s for Compositional Verification
• A simplified lower bound for context-free-language recognition
• A lower bound for the nondeterministic space complexity of context-free recognition
• Exact DFA Identification Using SAT Solvers
• Recognition of tractable DNFs representable by a constant number of intervals
• Upper bounds on recognition of a hierarchy of non-context-free languages
• Efficient algorithms for the inference of minimum size DFAs
• A sufficient condition to polynomially compute a minimum separating DFA
• The recognition of deterministic CFLs in small time and space
• scientific article; zbMATH DE number 3958761

Cites work

• scientific article; zbMATH DE number 3427224 (Why is no real title available?)
• Beyond hyper-minimisation -- minimising DBAs and DPAs is NP-complete
• Certifying inexpressibility
• Complexity of automaton identification from given data
• Computing minimal separating DFAs and regular invariants using SAT and SMT solvers
• Efficient separability of regular languages by subsequences and suffixes
• Exact DFA Identification Using SAT Solvers
• Fixing the state budget: approximation of regular languages with small DFAs
• Inferring regular languages and \(\omega\)-languages
• Learning regular sets from queries and counterexamples
• Linear Automaton Transformations
• Model checking of safety properties
• Recognizing safety and liveness
• Regular separability of well-structured transition systems
• Separating regular languages with first-order logic
• Solving Sequential Conditions by Finite-State Strategies
• State Reduction in Incompletely Specified Finite-State Machines
• Tools and Algorithms for the Construction and Analysis of Systems

Cited in

(2)

• Exact DFA Identification Using SAT Solvers
• DFA with a Bounded Activity Level

This page was built for publication: Certifying DFA bounds for recognition and separation

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