Inductive Certificate Synthesis for Control Design

摘要: The focus of this thesis is developing a framework for designing correct-by-construction controllers using control certificates. We use nonlinear dynamical systems to model the physical environment (plants). goal synthesize these plants while guaranteeing formal correctness w.r.t. given specifications. consider different fundamental specifications including stability, safety, and reach-while-stay. Stability specification states that execution traces system remain close an equilibrium state approach it asymptotically. Safety requires stay in safe region. Finally, reach-while-stay specification, safety needed until target set reached. The design task consists two phases. In first phase, problem reduced question finding certificate. More precisely, phase define class certificates with specific structure. This definition should guarantee following: "Having certificate, one can systematically controller prove its at same time." second find such potential certificate space (hypothesis space) parameterized functions. Next, we provide inductive search proper parameters, which yield Finally, evaluate our framework. show discovering practically feasible demonstrate effectiveness automatically designed through simulations real experiments.