SAT-solving in practice, with a tutorial example from supervisory control

DOI10.1007/s10626-009-0081-8zbMath1180.93065MaRDI QIDQ843991

Niklas Sörensson, Alexey Voronov, Koen Claessen, Knut Åkesson, Mary Sheeran, Niklas Een

Publication date: 18 January 2010

Published in: Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL: https://research.chalmers.se/en/publication/98185

zbMATH Keywords

supervisory control; formal verification; model checking; Boolean satisfiability problem

Mathematics Subject Classification ID

93C83: Control/observation systems involving computers (process control, etc.)

93A13: Hierarchical systems

93C65: Discrete event control/observation systems

Related Items

Accelerating a continuous-time analog SAT solver using GPUs, Explaining the \texttt{cumulative} propagator, SAT-solving in practice, with a tutorial example from supervisory control, The possibilistic Horn non-clausal knowledge bases

Uses Software

• MiniSat
• SATO
• Chaff
• BerkMin
• UMDES

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Optimal speedup of Las Vegas algorithms
• SAT-solving in practice, with a tutorial example from supervisory control
• Graph-Based Algorithms for Boolean Function Manipulation
• Supervisory Control of a Class of Discrete Event Processes
• Formal Methods in Computer-Aided Design
• Correct Hardware Design and Verification Methods
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• The complexity of theorem-proving procedures
• Computer Aided Verification
• Computer Aided Verification