Deep Reinforcement Learning (DRL) has the potential to be used for synthesizing feedback controllers (agents) for various complex systems with unknown dynamics. These systems are expected to satisfy diverse safety and liveness properties best captured using temporal logic. In RL, the reward function plays a crucial role in specifying the desired behaviour of these agents. However, the problem of designing the reward function for an RL agent to satisfy complex temporal logic specifications has received limited attention in the literature. To address this, we provide a systematic way of generating rewards in real-time by using the quantitative semantics of Signal Temporal Logic (STL), a widely used temporal logic to specify the behaviour of cyber-physical systems. We propose a new quantitative semantics for STL having several desirable properties, making it suitable for reward generation. We evaluate our STL-based reinforcement learning mechanism on several complex continuous control benchmarks and compare our STL semantics with those available in the literature in terms of their efficacy in synthesizing the controller agent. Experimental results establish our new semantics to be the most suitable for synthesizing feedback controllers for complex continuous dynamical systems through reinforcement learning.

The growing use of complex Cyber-Physical Systems (CPSs) in safety-critical applications has led to the demand for the automatic synthesis of robust feedback controllers that satisfy a given set of formal specifications. Controller synthesis from the high-level specification is an NP-Hard problem. We propose a heuristic-based automated technique that synthesizes feedback controllers guided by Signal Temporal Logic (STL) specifications. Our technique involves rigorous analysis of the traces generated by the closed-loop system, matrix decomposition, and an incremental multi-parameter tuning procedure. In case a controller cannot be found to satisfy all the specifications, we propose a technique for modifying the unsatisfiable specifications so that the controller synthesized for the satisfiable subset of specifications now also satisfies the modified specifications. We demonstrate our technique on eleven controllers used as standard closed-loop control system benchmarks, including complex controllers having multiple independent or nested control loops. Our experimental results establish that the proposed algorithm can automatically solve complex feedback controller synthesis problems within a few minutes.

Simulink/Stateflow is the de facto tool for developing software for safety-critical real-time cyber-physical systems (CPSs). In Simulink, the model of a CPS is captured in a block diagram-based language, the model is simulated using the associated simulators and then the software code is generated automatically for the embedded controller. The presence of a bug in the Simulink model may lead to catastrophic failure during the execution of the system developed based on the model. Unlike in application software, finding bugs in Simulink models is challenging due to the hybrid nature of the model. We present an automated debugging methodology of a CPS model captured in Simulink. Our methodology has two main components-bug localization and model repair. For bug localization, we capture the requirements of the system in signal temporal logic (STL) and employ the runtime monitoring technique to generate a trace that violates the specification. The violating trace is used to identify the internal signals that have the potential to contribute to the violation. For precise bug localization by narrowing down the offending signals, we employ a matrix decomposition technique to find the signals contributing to the bug accurately. Our bug localization technique is precise enough to enable us to repair the model. If the bug is due to an inappropriate value for a model parameter, we employ a parameter tuning method to find a value for the parameter that repairs the model automatically. We carry out numerous case studies on Simulink models obtained from different sources and demonstrate that our automated debugging technology can fix the bugs in the Simulink models effectively.