  Prior work on automatic control synthesis for cyber-physical systems under
logical constraints has primarily focused on environmental disturbances or
modeling uncertainties, however, the impact of deliberate and malicious attacks
has been less studied. In this paper, we consider a discrete-time dynamical
system with a linear temporal logic (LTL) constraint in the presence of an
adversary, which is modeled as a stochastic game. We assume that the adversary
observes the control policy before choosing an attack strategy. We investigate
two problems. In the first problem, we synthesize a robust control policy for
the stochastic game that maximizes the probability of satisfying the LTL
constraint. A value iteration based algorithm is proposed to compute the
optimal control policy. In the second problem, we focus on a subclass of LTL
constraints, which consist of an arbitrary LTL formula and an invariant
constraint. We then investigate the problem of computing a control policy that
minimizes the expected number of invariant constraint violations while
maximizing the probability of satisfying the arbitrary LTL constraint. We
characterize the optimality condition for the desired control policy. A policy
iteration based algorithm is proposed to compute the control policy. We
illustrate the proposed approaches using two numerical case studies.
