%ARamasubramanian, B%ANiu, L.%AClark, A%ABushnell, L%APoovendran, R%D2019%I %K %MOSTI ID: 10131728 %PMedium: X %TLinear Temporal Logic Satisfaction in Adversarial Environments Using Secure Control Barrier Certificates %XThis 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. Country unknown/Code not availablehttps://doi.org/https://doi.org/10.1007/978-3-030-32430-8_23OSTI-MSA