查看文章

Signal Temporal Logic (STL)[10] has been increasingly employed to formalize complex properties for Cyber-Physical Systems (CPS). The power of STL is in its capability of expressing real (dense) time properties for real-valued signals (trajectories), unlike other popular logics, eg, Linear Temporal Logic (LTL)[1] and LTL over finite traces (LTLf)[3], that can reason only about events over discrete time. This power, however, comes with major challenges in control synthesis both theoretically and computationally. That is why, while there exist various methods for LTL control synthesis for complex and even uncertain dynamics [2, 9], existing STL synthesis methods are generally bounded to simple dynamics (and linear predicate functions) with limited uncertainty. In our ongoing work, we focus on these challenges and aim to develop a general framework for STL control synthesis that can handle high complexity as well as …