This paper studies the synthesis of control
policies for an agent that has to satisfy a temporal logic
specification in a partially observable environment, in
the presence of an adversary. The interaction of the
agent (defender) with the adversary is modeled as a
partially observable stochastic game. The search for
policies is limited to over the space of finite state
controllers, which leads to a tractable approach to
determine policies. The goal is to generate a defender
policy to maximize satisfaction of a given temporal logic
specification under any adversary policy. We relate the
satisfaction of the specification in terms of reaching (a
subset of) recurrent states of a Markov chain. We then
present a procedure to determine a set of defender and
adversary finite state controllers of given sizes that will
satisfy the temporal logic specification. We illustrate our
approach with an example.
more »
« less
Linear Temporal Logic Satisfaction in Adversarial Environments Using Secure Control Barrier Certificates
This paper studies the satisfaction of a class of temporal
properties for cyber-physical systems (CPSs) over a finite-time horizon
in the presence of an adversary, in an environment described by discretetime
dynamics. The temporal logic specification is given in safe−LTLF ,
a fragment of linear temporal logic over traces of finite length. The interaction
of the CPS with the adversary is modeled as a two-player zerosum
discrete-time dynamic stochastic game with the CPS as defender.
We formulate a dynamic programming based approach to determine a
stationary defender policy that maximizes the probability of satisfaction
of a safe − LTLF formula over a finite time-horizon under any stationary
adversary policy. We introduce secure control barrier certificates
(S-CBCs), a generalization of barrier certificates and control barrier certificates
that accounts for the presence of an adversary, and use S-CBCs
to provide a lower bound on the above satisfaction probability. When
the dynamics of the evolution of the system state has a specific underlying
structure, we present a way to determine an S-CBC as a polynomial
in the state variables using sum-of-squares optimization. An illustrative
example demonstrates our approach.
more »
« less
- Award ID(s):
- 1656981
- NSF-PAR ID:
- 10131728
- Date Published:
- Journal Name:
- IEEE Conference on Decision and Game Theory for Security
- Page Range / eLocation ID:
- 385-403
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
more » « less
This paper studies the synthesis of controllers for cyber-physical systems (CPSs) that are required to carry out complex time-sensitive tasks in the presence of an adversary. The time-sensitive task is specified as a formula in the metric interval temporal logic (MITL). CPSs that operate in adversarial environments have typically been abstracted as stochastic games (SGs); however, because traditional SG models do not incorporate a notion of time, they cannot be used in a setting where the objective is time-sensitive. To address this, we introduce durational stochastic games (DSGs). DSGs generalize SGs to incorporate a notion of time and model the adversary’s abilities to tamper with the control input (actuator attack) and manipulate the timing information that is perceived by the CPS (timing attack). We define notions of spatial, temporal, and spatio-temporal robustness to quantify the amounts by which system trajectories under the synthesized policy can be perturbed in space and time without affecting satisfaction of the MITL objective. In the case of an actuator attack, we design computational procedures to synthesize controllers that will satisfy the MITL task along with a guarantee of its robustness. In the presence of a timing attack, we relax the robustness constraint to develop a value iteration-based procedure to compute the CPS policy as a finite-state controller to maximize the probability of satisfying the MITL task. A numerical evaluation of our approach is presented on a signalized traffic network to illustrate our results.
-
more » « less
Security of cyber-physical systems (CPS) continues to pose new challenges due to the tight integration and operational complexity of the cyber and physical components. To address these challenges, this article presents a domain-aware, optimization-based approach to determine an effective defense strategy for CPS in an automated fashion—by emulating a strategic adversary in the loop that exploits system vulnerabilities, interconnection of the CPS, and the dynamics of the physical components. Our approach builds on an adversarial decision-making model based on a Markov Decision Process (MDP) that determines the optimal cyber (discrete) and physical (continuous) attack actions over a CPS attack graph. The defense planning problem is modeled as a non-zero-sum game between the adversary and defender. We use a model-free reinforcement learning method to solve the adversary’s problem as a function of the defense strategy. We then employ Bayesian optimization (BO) to find an approximate
best-response for the defender to harden the network against the resulting adversary policy. This process is iterated multiple times to improve the strategy for both players. We demonstrate the effectiveness of our approach on a ransomware-inspired graph with a smart building system as the physical process. Numerical studies show that our method converges to a Nash equilibrium for various defender-specific costs of network hardening. -
Many systems are naturally modeled as Markov Decision Processes (MDPs), combining probabilities and strategic actions. Given a model of a system as an MDP and some logical specification of system behavior, the goal of synthesis is to find a policy that maximizes the probability of achieving this behavior. A popular choice for defining behaviors is Linear Temporal Logic (LTL). Policy synthesis on MDPs for properties specified in LTL has been well studied. LTL, however, is defined over infinite traces, while many properties of interest are inherently finite. Linear Temporal Logic over finite traces (LTLf ) has been used to express such properties, but no tools exist to solve policy synthesis for MDP behaviors given finite-trace properties. We present two algorithms for solving this synthesis problem: the first via reduction of LTLf to LTL and the second using native tools for LTLf . We compare the scalability of these two approaches for synthesis and show that the native approach offers better scalability compared to existing automaton generation tools for LTL.more » « less
-
null (Ed.)We present a data-driven framework for strategy synthesis for partially-known switched stochastic systems. The properties of the system are specified using linear temporal logic (LTL) over finite traces (LTLf), which is as expressive as LTL and enables interpretations over finite behaviors. The framework first learns the unknown dynamics via Gaussian process regression. Then, it builds a formal abstraction of the switched system in terms of an uncertain Markov model, namely an Interval Markov Decision Process (IMDP), by accounting for both the stochastic behavior of the system and the uncertainty in the learning step. Then, we synthesize a strategy on the resulting IMDP that maximizes the satisfaction probability of the LTLf specification and is robust against all the uncertainties in the abstraction. This strategy is then refined into a switching strategy for the original stochastic system. We show that this strategy is near-optimal and provide a bound on its distance (error) to the optimal strategy. We experimentally validate our framework on various case studies, including both linear and non-linear switched stochastic systems.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/https://doi.org/10.1007/978-3-030-32430-8_23
