Control Closure Certificates

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.