Control Closure Certificates

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 $\omega$-regular specifications. Typical functional approaches to synthesize controllers against $\omega$-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 $\omega$-regular specifications. We build on this notion to synthesize controllers to ensure the satisfaction of $\omega$-regular specifications. To do so, we first illustrate how one may construct control closure certificates to visit a region infinitely often (or only finitely often) via disjunctive well-founded arguments. We then combine these arguments to provide an argument for parity specifications. Thus, finding an appropriate control closure certificate over the product of the system and a parity automaton specifying a desired $\omega$-regular specification ensures that there exists a controller $\kappa$ to enforce the $\omega$-regular specification. We propose a sum-of-squares optimization approach to synthesize such certificates and demonstrate their efficacy in designing controllers over some case studies.