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
Secure Control Under Partial Observability with Temporal Logic Constraints
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
- Award ID(s):
- 1656981
- NSF-PAR ID:
- 10131730
- Date Published:
- Journal Name:
- American Control Conference (ACC)
- 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.
-
We study the problem of inverse reinforcement learning (IRL), where the learning agent recovers a reward function using expert demonstrations. Most of the existing IRL techniques make the often unrealistic assumption that the agent has access to full information about the environment. We remove this assumption by developing an algorithm for IRL in partially observable Markov decision processes (POMDPs). The algorithm addresses several limitations of existing techniques that do not take the information asymmetry between the expert and the learner into account. First, it adopts causal entropy as the measure of the likelihood of the expert demonstrations as opposed to entropy in most existing IRL techniques, and avoids a common source of algorithmic complexity. Second, it incorporates task specifications expressed in temporal logic into IRL. Such specifications may be interpreted as side information available to the learner a priori in addition to the demonstrations and may reduce the information asymmetry. Nevertheless, the resulting formulation is still nonconvex due to the intrinsic nonconvexity of the so-called forward problem, i.e., computing an optimal policy given a reward function, in POMDPs. We address this nonconvexity through sequential convex programming and introduce several extensions to solve the forward problem in a scalable manner.This scalability allows computing policies that incorporate memory at the expense of added computational cost yet also outperform memoryless policies. We demonstrate that, even with severely limited data, the algorithm learns reward functions and policies that satisfy the task and induce a similar behavior to the expert by leveraging the side information and incorporating memory into the policy.more » « less
-
null (Ed.)Moving target defense (MTD) is a proactive defense approach that aims to thwart attacks by continuously changing the attack surface of a system (e.g., changing host or network configurations), thereby increasing the adversary’s uncertainty and attack cost. To maximize the impact of MTD, a defender must strategically choose when and what changes to make, taking into account both the characteristics of its system as well as the adversary’s observed activities. Finding an optimal strategy for MTD presents a significant challenge, especially when facing a resourceful and determined adversary who may respond to the defender’s actions. In this paper, we propose a multi-agent partially-observable Markov Decision Process model of MTD and formulate a two-player general-sum game between the adversary and the defender. To solve this game, we propose a multi-agent reinforcement learning framework based on the double oracle algorithm. Finally, we provide experimental results to demonstrate the effectiveness of our framework in finding optimal policies.more » « less
-
Linear temporal logic (LTL) with the knowledge operator, denoted as KLTL, is a variant of LTL that incorporates what an agent knows or learns at run-time into its specification. Therefore it is an appropriate logical formalism to specify tasks for systems with unknown components that are learned or estimated at run-time. In this paper, we consider a linear system whose system matrices are unknown but come from an a priori known finite set. We introduce a form of KLTL that can be interpreted over the trajectories of such systems. Finally, we show how controllers that guarantee satisfaction of specifications given in fragments of this form of KLTL can be synthesized using optimization techniques. Our results are demonstrated in simulation and on hardware in a drone scenario where the task of the drone is conditioned on its health status, which is unknown a priori and discovered at run-time.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- https://doi.org/https://doi.org/10.23919/ACC.2019.8814630
