We introduce a novel learning-based approach to synthesize safe and robust controllers for autonomous Cyber-Physical Systems and, at the same time, to generate challenging tests. This procedure combines formal methods for model verification with Generative Adversarial Networks. The method learns two Neural Networks: the first one aims at generating troubling scenarios for the controller, while the second one aims at enforcing the safety constraints. We test the proposed method on a variety of case studies.
defender, which in turn tries to learn how to face them without violating some safety constraints. The outcome of this training procedure is twofold: on one side we get a robust controller, whereas on the other we get a generator of adverse tests.
The learned controller is a black-box device that should be able to deal with adverse or unobserved
scenarios, but that does not provide worst-case guarantees. In this regard one could additionally rely on a
shield-based approach, as proposed in [
Safety of a system is guaranteed by the satisfaction of a set of requirements. Checking the satisfiability
of properties in hybrid systems, where both discrete and continuous components are involved, is often
too computationally complex or undecidable [
We model the interaction of an agent with an adversarial environment as a zero-sum game, similarly
to the strategy behind GANs [
Agent-Environment Model. Due to coexistence of continuous and discrete components, CPSs are typically represented as hybrid models: the continuous part is represented by differential equations that describe the behaviour of the plant; the discrete part, instead, identifies the possible states of the controller. We decompose our model in two interacting parts: the agent a and the environment e. Both of them are able to observe at least part of the whole state space S, i.e. they are aware of some observable states O ⊂ S. By distinguishing between the observable states of the agent Oa ⊆ O and of the environment Ob ⊆ O, we are able to force uneven levels of knowledge between them.
Let Ua and Ue be the spaces of all possible actions for the two components. We discretize the evolution of the system as a discrete-time system with step Δt, which evolves according to a function ψ : S × Ua × Ue × R −→ S. By taking control actions at fixed time intervals of length Δt, we obtain a discrete evolution of the form si+1 = si + ψ(si, uia, uie, ti), where ti := t0 + i · Δt, ui := u(ti) and si := s(ti). Therefore, we are able to simulate the entire evolution of the system over a time horizon H via ψ and to obtain a complete trajectory ξ = s0 . . . sH−1 in the state space. Optimization strategy. The proposed framework builds on GAN architectural design, in which two NNs compete in a minmax game to reach opposite goals. One network, denoted by A, represents the attacker, while the other, denoted by D, represents the defender. The aim of the former is to generate environment configurations in which the defender is not able to act safely, whereas, the latter tries to keep the CPS as safe as possible. In practice, the defender D can be interpreted as a controller for the agent. The safety requirement is expressed as a Signal Temporal Logic formula Φ over a finite time horizon H. We are leveraging the notion of robustness in quantitative semantics to measure the satisfiability of the STL property and to determine how safe the system is in a given configuration. We denote robustness as a function RΦ : SH → R, measuring the maximum shift that can be applied to a given trajectory ξ = s0 . . . sH−1 without violating the requirements of Φ. It is straightforward to use this measure as the objective function in the minmax game. When the system is in a state s0, the evolution of ξ is obtained by evaluating ψ at time steps ti = t0, . . . , tH−1 over two sequences of actions ua = (u0a, . . . , uaH−1) and ue = (ue0, . . . , ueH−1). We introduce two policy functions, ΠA for the attacker and ΠD for the defender, with the aim of reducing the output dimension. The two policies ΠA : ΘA × R → Ue and ΠD : ΘD × R → Ua are represented by a finite set of basis functions of time, with coefficients given by the output of the networks; in this work they are polynomial functions. For example, ΠA can encode the output θA of network A as a polynomial function of degree dA and the resulting ue(t) is evaluated at each time step, from t0 to tH−1, to produce the desired sequence of actions ue. The same reasoning holds for ΠD and ua. These policies have the benefit of producing a smoothing of the chosen actions, that prevents incoherent behaviours at subsequent instants.
Let wA be the weights of the attacker’s network A and wD the weights of the defender’s network D. The formalism introduced by the two policies transfers the problem of finding the best sequences of actions, ua and ue, to that of finding the best networks’ parameters, wD and wA. The minmax game can now be expressed in terms of the loss function L (wA, wD) = −RΦ(s0, wD, wA) as min max L (wA, wD).
wD wA
In this setting, the defender aims at generating safe actions by tuning its weights in favour of a loss minimization (i.e. robustness maximization). The attacker, instead, aims at generating troubling scenarios for the opponent by maximizing the loss (i.e., minimizing the robustness). 3
Car platooning. A platoon [
Results. Car platooning problem trivially extends to the case of n cars, where the first one is the leader and each of the other cars simply follows the one in front. Our simulations start from an initial configuration of equispaced vehicles, thus the first couple of subsequent cars acts as described in the two-cars model, while the other followers are controlled by copies of the same defender’s network.
This model has been tested in four different adverse configurations. The leader in Figure 1 acts according to the attacker’s policy, with sudden accelerations and brakes, and all followers are able to manage the unpredictable behaviour of the attacker by maintaining their relative distances within the safety range. We ran 10k simulations of different trajectories for each possible scenario. At each time step we computed the total percentage of safe trajectories and 100% of them achieved positive robustness. 4
Classical control theory fails in giving adequate safety guarantees in many complex real world scenarios. New reinforcement learning techniques aim at modelling the behaviour of complex systems and learning optimal controllers from the observed data. Therefore, they are particularly suitable for stochastic optimal control problems where the transition dynamics and the reward functions are unknown. We proposed a new learning technique, whose architecture is inspired by Generative Adversarial Networks, and tested its full potential against the vehicle platooning problem. Our approach has been able to enforce safety of the model, while also gaining insights about adverse configurations of the environment. As future work, we plan to test more scenarios and investigate the scalability of this approach. We also plan to extend this control synthesis strategy to stochastic hybrid systems.1