Characterization, Verification and Computation of Robust Controlled Invariants for Monotone Dynamical Systems
In this paper, we consider the problem of computing robust controlled invariants for discrete-time monotone dynamical systems. We consider different classes of monotone systems depending on whether the sets of states, control inputs and disturbances respect a given partial order. Then, we present set-based and trajectory-based characterizations of robust controlled invariants for the considered class of systems. Based on these characterizations, we propose algorithmic approaches for the verification and computation of robust controlled invariants. Finally, illustrative examples are provided showing the merits of the proposed approach.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
On Robust Controlled Invariants for Continuous-time Monotone Systems
This paper delves into the problem of computing robust controlled invariants for monotone continuous-time systems, with a specific focus on lower-closed specifications. We consider the classes of state monotone (SM) and …
Adaptive Inferential Method for Monotone Graph Invariants
We consider the problem of undirected graphical model inference. In many applications, instead of perfectly recovering the unknown graph structure, a more realistic goal is to infer some graph invariants (e.g., the maxim…
validNot All Invariants Are Equal: Curating Training Data to Accelerate Program Verification with SLMs
The synthesis of inductive loop invariants remains a critical bottleneck in automated program verification. While Large Language Models (LLMs) show promise in mitigating this issue, they often fail on complex programs, p…
On Scaling Data-Driven Loop Invariant Inference
Automated synthesis of inductive invariants is an important problem in software verification. Once all the invariants have been specified, software verification reduces to checking of verification conditions. Although st…
On Completeness of SDP-Based Barrier Certificate Synthesis over Unbounded Domains
Barrier certificates, serving as differential invariants that witness system safety, play a crucial role in the verification of cyber-physical systems (CPS). Prevailing computational methods for synthesizing barrier cert…