In safety-critical systems,it is desirable to automatically synthesize controllers for complex tasks with guaranteed safety and correctness.Although much progress has been made through controller synthesis from tempor...In safety-critical systems,it is desirable to automatically synthesize controllers for complex tasks with guaranteed safety and correctness.Although much progress has been made through controller synthesis from temporal logic speci-cations,existing approaches generally require conservative assumptions and do not scale well with system dimensionality.We propose a scalable,provably complete algorithm that synthesizes continuous trajectories for hybrid systems to satisfy temporal logic speci-cations.Speci-cally,we harness highly e±cient Boolean satis-ability(SAT)and Linear Programming(LP)solvers to-nd trajectories that satisfy nonconvex Signal Temporal Logic(STL)speci-cations for a class of high dimensional hybrid systems.The proposed design algorithms are proven sound and complete,and are validated in simulation experiments.展开更多
基金support of the National Science Foundation(Grant No.IIS-1724070,CNS-1830335,IIS-2007949)is gratefully acknowledged.
文摘In safety-critical systems,it is desirable to automatically synthesize controllers for complex tasks with guaranteed safety and correctness.Although much progress has been made through controller synthesis from temporal logic speci-cations,existing approaches generally require conservative assumptions and do not scale well with system dimensionality.We propose a scalable,provably complete algorithm that synthesizes continuous trajectories for hybrid systems to satisfy temporal logic speci-cations.Speci-cally,we harness highly e±cient Boolean satis-ability(SAT)and Linear Programming(LP)solvers to-nd trajectories that satisfy nonconvex Signal Temporal Logic(STL)speci-cations for a class of high dimensional hybrid systems.The proposed design algorithms are proven sound and complete,and are validated in simulation experiments.
