# Secure Control under Partial Observability with Temporal Logic Constraints

## TL;DR

This paper develops a method for synthesizing control policies for agents with partial observability to satisfy temporal logic specifications in adversarial stochastic environments, using finite state controllers for tractability.

## Contribution

It introduces a novel approach to generate defender policies in partially observable stochastic games with temporal logic constraints, focusing on finite state controllers.

## Key findings

- The approach effectively synthesizes policies satisfying temporal logic specifications.
- Finite state controllers enable tractable policy synthesis in complex environments.
- The method is demonstrated through a detailed example.

## Abstract

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.