Control Closure Certificates
Vishnu Murali, Mohammed Adib Oumer, Majid Zamani

TL;DR
This paper introduces control closure certificates, a novel automated method for synthesizing controllers that ensure discrete-time control systems satisfy complex $oldsymbol{ ext{omega}}$-regular specifications, using sum-of-squares optimization.
Contribution
It develops the concept of control closure certificates for controller synthesis against $oldsymbol{ ext{omega}}$-regular specifications, extending transition invariants with a practical, automated approach.
Findings
Effective sum-of-squares optimization method for synthesis.
Successful case studies demonstrating controller design.
Certificates ensure satisfaction of $oldsymbol{ ext{omega}}$-regular specifications.
Abstract
This paper introduces the notion of control closure certificates to synthesize controllers for discrete-time control systems against -regular specifications. Typical functional approaches to synthesize controllers against -regular specifications rely on combining inductive invariants (for example, via barrier certificates) with proofs of well-foundedness (for example, via ranking functions). Transition invariants, provide an alternative where instead of standard well-foundedness arguments one may instead search for disjunctive well-foundedness arguments that together ensure a well-foundedness argument. Closure certificates, functional analogs of transition invariants, provide an effective, automated approach to verify discrete-time dynamical systems against linear temporal logic and -regular specifications. We build on this notion to synthesize controllers to…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
