Control Closure Certificates
摘要
This paper introduces the notion of control closure certificates ( \(\text {C}^3\) ) 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 \(\text {C}^3\) 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.