Signal Temporal Logic (STL) is a widely adopted specification language for Cyber-Physical Systems that can be used to express critical temporal requirements, such as system safety and response time. STL’s expressivity, however, is not sufficient to capture the cumulative duration during which a property holds within an interval of time. To overcome this limitation, we introduce Cumulative-Time Signal Temporal Logic (CT-STL) which operates over discrete-time signals and extends STL with a new cumulative-time operator. This operator compares the sum of all timesteps for which its nested formula is true with a threshold. We present both a qualitative and a quantitative (robustness) semantics for CT-STL and prove the soundness and completeness of the robustness semantics. We also provide an efficient online monitoring algorithm for both semantics. We demonstrate the utility of CT-STL via two case studies: specifying and monitoring cumulative temporal requirements for a microgrid and an artificial pancreas.

Abstract We show how a symmetric and fully distributed flocking controller can be synthesized using Deep Learning from a centralized flocking controller. Our approach is based on Supervised Learning, with the centralized controller providing the training data, in the form of trajectories of state-action pairs. We use Model Predictive Control (MPC) for the centralized controller, an approach that we have successfully demonstrated on flocking problems. MPC-based flocking controllers are high-performing but also computationally expensive. By learning a symmetric and distributed neural flocking controller from a centralized MPC-based one, we achieve the best of both worlds: the neural controllers have high performance (on par with the MPC controllers) and high efficiency. Our experimental results demonstrate the sophisticated nature of the distributed controllers we learn. In particular, the neural controllers are capable of achieving myriad flocking-oriented control objectives, including flocking formation, collision avoidance, obstacle avoidance, predator avoidance, and target seeking. Moreover, they generalize the behavior seen in the training data to achieve these objectives in a significantly broader range of scenarios. In terms of verification of our neural flocking controller, we use a form of statistical model checking to compute confidence intervals for its convergence rate and time to convergence.