Automated formal synthesis of provably safe digital controllers for continuous plants

Area of Science:

• Control Theory
• Formal Methods
• Computer Science

Background:

• Digital controllers are essential for physical systems.
• Ensuring controller safety, especially with finite-precision arithmetic, is challenging.
• Existing methods may not fully address safety guarantees.

Purpose of the Study:

• To present a sound and automated approach for synthesizing safe digital controllers.
• To account for the impact of finite-precision arithmetic in controller synthesis.
• To ensure controllers stabilize physical plants while maintaining safety.

Main Methods:

• Utilizing counterexample-guided inductive synthesis.
• Employing an inductive generalization phase to produce stabilizing controllers.
• Implementing bounded model checking for safety verification and counterexample generation.

Main Results:

• Successfully synthesized safe digital controllers for physical plant models.
• The approach iteratively refines controllers until safety is guaranteed.
• Demonstrated practical value using models from digital control literature.

Conclusions:

• The presented approach offers a robust method for automated safe controller synthesis.
• Finite-precision arithmetic effects are effectively managed within the synthesis process.
• This work advances the development of reliable digital control systems.