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

DOI10.1007/s10626-009-0081-8zbMath1180.93065OpenAlexW2100637096MaRDI 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 controlformal verificationmodel checkingBoolean satisfiability problem

Mathematics Subject Classification ID

Control/observation systems involving computers (process control, etc.) (93C83) Hierarchical systems (93A13) Discrete event control/observation systems (93C65)

Related Items (4)

SAT-solving in practice, with a tutorial example from supervisory control ⋮ Accelerating a continuous-time analog SAT solver using GPUs ⋮ Explaining the \texttt{cumulative} propagator ⋮ 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

This page was built for publication: SAT-solving in practice, with a tutorial example from supervisory control