.png){kind=icon}
.png){kind=icon}
Return
Control Closure Certificates
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-08707-2_18.png)
.png){kind=icon}
Original request for help.png){kind=icon}
Share.png){kind=icon}
Save
Abstract
En 中文
This paper introduces the notion of control closure certificates (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 C(3)over the product of the system and a parity automaton specifying a desired omega-regular specification ensures that there exists a controller 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.
Keywords:
discrete-time control systems
transition invariants
controlsynthesis
w-regular properties
parityautomata
Journal
A
IF:
0
Papers:
21
Citations:
0
