Computing minimal separating DFAs and regular invariants using SAT and SMT solvers

DOI10.1007/978-3-642-33386-6_28MaRDI QIDQ4649308zbMATH OpenOpenAlexFDO

Authors Daniel Neider

Publication date 21 November 2012

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-33386-6_28

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Integer programming (90C10)

Recommendations

• Learning Minimal Separating DFA’s for Compositional Verification
• Exact DFA Identification Using SAT Solvers
• A sufficient condition to polynomially compute a minimum separating DFA
• Finding All Minimum-Size DFA Consistent with Given Examples: SAT-Based Approach
• Efficient symmetry breaking for SAT-based minimum DFA inference

Cited in

(12)

• Certifying DFA bounds for recognition and separation
• Efficient symmetry breaking for SAT-based minimum DFA inference
• A sufficient condition to polynomially compute a minimum separating DFA
• BFS-based symmetry breaking predicates for DFA identification
• Minimal consistent DFA revisited
• Exact DFA Identification Using SAT Solvers
• Learning Minimal Separating DFA’s for Compositional Verification
• Finding All Minimum-Size DFA Consistent with Given Examples: SAT-Based Approach
• Efficient algorithms for the inference of minimum size DFAs
• Privacy-preserving co-synthesis against sensor-actuator eavesdropping intruder
• Unsupervised automata learning via discrete optimization
• Offline supervisory control synthesis: taxonomy and recent developments

Describes a project that uses

Uses Software

• InvGen

This page was built for publication: Computing minimal separating DFAs and regular invariants using SAT and SMT solvers

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