Secure Control in Partially Observable Environments to Satisfy LTL Specifications

• 成果类型: Article
• 署名作者: Ramasubramanian, Bhaskar; Niu, Luyao; Clark, Andrew; Bushnell, Linda; Poovendran, Radha
• 署名单位: University of Washington; University of Washington Seattle; Worcester Polytechnic Institute
• 刊物名称: IEEE TRANSACTIONS ON AUTOMATIC CONTROL
• ISSN/ISSBN: 0018-9286
• DOI: 10.1109/TAC.2020.3039484
• 发表日期: 2021
• 页码: 5665-5679
• 关键词: Power capacitors; games; Markov processes; computers; semantics; Robot sensing systems; Power system stability; Finite-state controllers (FSCs); global Markov chain (GMC); linear temporal logic (LTL); partially observable stochastic games (POSGs); policy iteration; Stackelberg equilibrium; value iteration

摘要

This article 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 goal is to generate a defender policy to maximize satisfaction of a given temporal logic specification under any adversary policy. The search for policies is limited to the space of finite-state controllers, which leads to a tractable approach to determine policies. We relate the satisfaction of the specification to reaching (a subset of) recurrent states of a Markov chain. We present an algorithm to determine a set of defender and adversary finite-state controllers of fixed sizes that will satisfy the temporal logic specification and prove that it is sound. We then propose a value-iteration algorithm to maximize the probability of satisfying the temporal logic specification under finite-state controllers of fixed sizes. Finally, we extend this setting to the scenario where the size of the finite-state controller of the defender can be increased to improve the satisfaction probability. We illustrate our approach with an example.