Control Closure Certificates
Fuente:
arXiv
Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915430126321664 |
|---|---|
| author | Murali, Vishnu Oumer, Mohammed Adib Zamani, Majid |
| author_facet | Murali, Vishnu Oumer, Mohammed Adib Zamani, Majid |
| contents | 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 ensure the satisfaction of $ω$-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 $ω$-regular specification ensures that there exists a controller $κ$ to enforce the $ω$-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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_03947 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Control Closure Certificates Murali, Vishnu Oumer, Mohammed Adib Zamani, Majid Logic in Computer Science Systems and Control 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 ensure the satisfaction of $ω$-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 $ω$-regular specification ensures that there exists a controller $κ$ to enforce the $ω$-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. |
| title | Control Closure Certificates |
| topic | Logic in Computer Science Systems and Control |
| url | https://arxiv.org/abs/2508.03947 |