Linear temporal logic satisfaction in adversarial environments using secure control barrier certificates
From MaRDI portal
Publication:3297675
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.
Recommendations
- Temporal logic verification of stochastic systems using barrier certificates
- Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
- Temporal logic model predictive control
- Reactive synthesis from signal temporal logic specifications
- Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
Cites work
- A dynamic game approach to distributionally robust safety specifications for stochastic systems
- A Framework for Worst-Case and Stochastic Safety Verification Using Barrier Certificates
- A stochastic games framework for verification and control of discrete time stochastic hybrid systems
- An optimal one-way multigrid algorithm for discrete-time stochastic control
- Automata Theory Meets Barrier Certificates: Temporal Logic Verification of Nonlinear Systems
- Bisimulation Equivalence of Discrete-Time Stochastic Linear Control Systems
- Control Barrier Function Based Quadratic Programs for Safety Critical Systems
- Depth-First Search and Linear Graph Algorithms
- Formal methods for discrete-time dynamical systems
- Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems
- scientific article; zbMATH DE number 1243371 (Why is no real title available?)
- scientific article; zbMATH DE number 700091 (Why is no real title available?)
- scientific article; zbMATH DE number 2102704 (Why is no real title available?)
- scientific article; zbMATH DE number 2102731 (Why is no real title available?)
- scientific article; zbMATH DE number 5585443 (Why is no real title available?)
- Optimal Control of Markov Decision Processes With Linear Temporal Logic Constraints
- Probabilistic reachability and safety for controlled discrete time stochastic hybrid systems
- SDPT3 — A Matlab software package for semidefinite programming, Version 1.3
- Semidefinite programming relaxations for semialgebraic problems
- Sequential Stackelberg equilibria in two-person games
- Stochastic stability and control
- Symbolic reachability computation for families of linear vector fields
- Temporal logic verification of stochastic systems using barrier certificates
- The benefits of relaxing punctuality
- Timed temporal logics
Cited in
(2)
This page was built for publication: Linear temporal logic satisfaction in adversarial environments using secure control barrier certificates
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3297675)
