Control Synthesis for Cyber-Physical Systems to Satisfy MITL Objectives under Timing and Actuator Atta

This paper studies the synthesis of controllers for

cyber-physical systems (CPSs) that are required to carry out

complex tasks that are time-sensitive, in the presence of an

adversary. The task is specified as a formula in metric interval

temporal logic (MITL). The adversary is assumed to have the

ability to tamper with the control input to the CPS and also

manipulate timing information perceived by the CPS. In order

to model the interaction between the CPS and the adversary, and

also the effect of these two classes of attacks, we define an entity

called a durational stochastic game (DSG). DSGs probabilistically

capture transitions between states in the environment, and also

the time taken for these transitions. With the policy of the

defender represented as a finite state controller (FSC), we present

a value-iteration based algorithm that computes an FSC that

maximizes the probability of satisfying the MITL specification

under the two classes of attacks. A numerical case-study on a

signalized traffic network is presented to illustrate our results.