Linear Temporal Logic Satisfaction in Adversarial Environments using Secure Control Barrier Certificates

TL;DR

This paper develops a method to verify and maximize the probability of satisfying temporal logic specifications in cyber-physical systems operating in adversarial environments, using secure control barrier certificates and dynamic programming.

Contribution

It introduces secure control barrier certificates (S-CBCs) for adversarial settings and formulates a dynamic programming approach to optimize defender policies.

Findings

S-CBCs provide a lower bound on satisfaction probability.

The approach can compute S-CBCs as polynomial functions using sum-of-squares optimization.

An illustrative example demonstrates the effectiveness of the method.

Abstract

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 discrete-time dynamics. The temporal logic specification is given in safe-LTL_F, 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 zero-sum discrete-time dynamic stochastic game with the CPS as defender. We formulate a dynamic programming based approach to determine a stationary defender policy that maximized the probability of satisfaction of a safe-LTL_F 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.