There are two mainstream methods for acquiring DNN controllers, supervised learning and deep reinforcement learning (DRL). Supervised learning requires the collection of system executions of an original CPS, which serves as the training dataset. The training dataset provides a template to guide the DNN controller to mimic the behavior of the original CPS. Unlike supervised learning, DRL trains controllers using trial and error within an environment. The controller interacts with the environment, receiving feedback in the form of rewards for its actions. Through multiple iterations, the controller learns to optimize its actions to maximize the cumulative rewards. DRL employs neural networks, like deep Q-networks, to approximate the optimal action-selection policy.

To build AI-enabled CPSs to use as target of our approach, we proceed as follows. For each plant M described before, we consider two DNN controllers C, so to obtain two AI-enabled CPSs M^C. For AFC, we take the DNN trained by the authors of FalsifAI [1]. For ACC and WT, instead, we followed the approach explained in [1] and trained two feed-forward neural networks for each subject CPS. Table I reports the complexities of the 8 AI-enabled CPSs in terms of number of blocks of each M^C and number of weights of the controller C. In the following, a benchmark is given by an AI-enabled CPS M^C and a specification φ, identified as M^C_φ. So, in total there are 10 benchmarks.

As an important driving assistance function, ACC has been popularized in the automotive field after decades of development. The ACC system mentioned in this work is originally from MathWorks [2], and it aims to maintain a safe distance between the ego car and the lead car by adjusting the acceleration of the ego car. The ACC system takes the lead car’s acceleration as input and provides outputs in terms of the velocities and distances covered by both the lead and ego cars. The specification 𝜑^1_ACC requires that the relative distance d_rel between two cars must always be higher than the sum of the safe distance d_safe and the reaction distance reactDist (i.e., 1.4 × v_ego, where 1.4 is the time-gap [28]) of the ego car during the time interval [0,50], and that the speed of the ego car v_ego should always be lower than a given speed v_set. Here, d_safe and v_set are set to 10 and 30, respectively. 

DNN Controllers

The controllers takes three input signals: relative distance d_rel, relative speed v_rel and the velocity of ego car v_ego, and outputs an ego car acceleration a_ego as the control command. The figure right below is the expansion  of a controller instance.

Specification 1

The first specification of ACC is formulated as follows, saying that during the simulation, the relative distance, d_rel, between the two cars should always be larger than a safety distance, defined by the sum of a constant d_safe and the braking distance 1.4 ∗ v_ego of the ego car. Meanwhile, the speed should be lower than 30. 

𝜑^1_ACC ≡ □[0,50] (d_rel ≥ d_safe + reactDist ⋀ v_ego ≤ v_set) with reactDist = 1.4 × v_ego

Specification 2

The second specification of ACC is formulated as follows, saying that during the time interval [0, 45], if the relative distance d_rel is lower than the sum of the reaction distance of the ego car and a distance slightly above  the safe distance d_safe,  the system is on the edge of a hazardous state. In such circumstances, the system is required to recover from this state and return to a safe state within 5 seconds.

𝜑^2_ACC ≡ □[0, 45](d_rel < 12 + reactDist → ♢[0, 5](d_rel ≥ 12 + reactDist)) with reactDist = 1.4 × v_ego

Abstract Fuel Control (AFC) is a complex air-fuel control system released by Toyota [3]. The whole system takes two input signals from the outside environment, pedal angle PA and engine speed ES, and outputs μ = |AF - AF_ref|/AF_ref, which is the deviation of the air-to-fuel ratio AF from a reference value AF_ref. By changing PA and ES, the fuel controller should adjust the intake gas rate to the cylinder to maintain optimal air-to-fuel ratio. The goal of this system is to control the deviation μ no more than a predefined threshold.

DNN Controllers

The DNN controller takes engine speed ES, throttle angle TA, throttle flow MAF and measured airbyfuel λ as input signals, and outputs commanded fuel Fc as a control command. The figure right below is the expansion  of a controller instance.

Specification 1

The formula of the first specification is as follows, where μ, the deviation of the air-to-fuel ratio AF from a reference value AF_ref, should always be less than 0.15 during the time interval [0, 30]. Here AF_ref is a constant 14.7. 

𝜑^1_AFC ≡ □[0, 30](μ ≤ 0.15)

Specification 2

The second specification is described as follows: during the time interval [10, 28.5], the controller can bring the μ back to within 0.1, within a certain time period when μ exceeds 0.1 within 1.5 seconds.

𝜑^2_AFC ≡ □[10, 28.5] (μ > 0.1 → ♢[0,1.5] (μ ≤ 0.1))

SC is a component of an electric power system. During the condensation process of steam, it aims to keep the pressure in the condenser staying around a reference pressure. The external input of the system is the steam mass flow rate, while the system’s output  is the internal pressure of the condenser. 

Controllers

The DNN controller of SC takes the error error between pressure reference pressure_ref with real pressure pressure as input, and outputs control command action to regulate pressure. The figure right below is the expansion of a controller instance.

Specification 1

The specification is described as follows: the pressure should be maintained between 87 and 87.5 in the time interval [30, 35]. 

𝜑_SC ≡ □[30, 35](|pressure| >= 87 ∧ |pressure| <= 87.5)

As a container for controlling the inflow and outflow of water, Water Tank (WT) has been applied in the industry domain widely such as chemical industry. This system is collected from MathWorks [4]. This example includes the nonlinear Water-Tank System plant and a FFNN controller in a single-loop feedback system. Water enters the tank from the top at a rate proportional to the voltage applied to the pump. The water leaves through an opening in the tank base at a rate that is proportional to the square root of the water height in the tank. The presence of the square root in the water flow rate results in a nonlinear plant. The system takes the reference water level h_ref as input signal and outputs the actual water level h_out in real time.

DNN Controller

The DNN controller of WT takes four input signals: the absolute value of the error error between reference height h_ref with real height h_out, and outputs control command action to regulate water level. The figure right below is the expansion of a controller instance.

Specification 1

As shown below, the absolute value of the error error between reference height h_ref with real height h_out is demanded to be not greater than 0.86 within the interval [4, 5], [9, 10] and [14, 15].

𝜑_WT ≡ □I(|error| ≤ 0.86)  I = [4, 5] ⋀ [9, 10] ⋀ [14, 15]

[1] Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo, and Jianjun Zhao. 2023. FalsifAI: Falsification of AI-Enabled Hybrid Control Systems Guided by Time-Aware Coverage Criteria. IEEE Transactions on Software Engineering 49, 4 (2023), 1842–1859. https://doi.org/10.1109/TSE.2022.3194640  

[2] Mathworks. 2023. Adaptive Cruise Control System Using Model Predictive Control. https://www.mathworks.com/help/mpc/ug/adaptive-cruise-control- using- model- predictive- controller.html

[3] Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and Ken Butts. Powertrain control verification benchmark. In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC ’14, pages 253–262, New York, NY, USA, 2014. ACM.

[4] Mathworks. 2023. Watertank Simulink Model. https://www.mathworks.com/ help/slcontrol/gs/watertank- simulink- model.html