This paper studies temporal planning in probabilistic environments, modeled as labeled Markov decision processes (MDPs), with user preferences over multiple temporal goals. Existing works reflect such preferences as a prioritized list of goals. This paper introduces a new specification language, termed prioritized qualitative choice linear temporal logic on finite traces, which augments linear temporal logic on finite traces with prioritized conjunction and ordered disjunction from prioritized qualitative choice logic. This language allows for succinctly specifying temporal objectives with corresponding preferences accomplishing each temporal task. The finite traces that describe the system's behaviors are ranked based on their dissatisfaction scores with respect to the formula. We propose a systematic translation from the new language to a weighted deterministic finite automaton. Utilizing this computational model, we formulate and solve a problem of computing an optimal policy that minimizes the expected score of dissatisfaction given user preferences. We demonstrate the efficacy and applicability of the logic and the algorithm on several case studies with detailed analyses for each.

In this paper, we study the use of deception for strategic planning in adversarial environments. We model the interaction between the agent (player 1) and the adversary (player 2) as a two-player concurrent stochastic game in which the adversary has incomplete information about the agent’s task specification given as a temporal logic formula. During the interaction, the adversary can infer the agent’s intention from observations and adapt its strategy so as to prevent the agent from satisfying the objective. To plan against such an adaptive opponent, the agent must leverage its knowledge about the adversary’s incomplete information to influence the behavior of the opponent, and thereby be deceptive. To synthesize a deceptive strategy, we introduce a class of hypergame models that capture the interaction between the agent and its adversary given asymmetric, incomplete information. We develop a solution concept for this class of hypergames and show that the subjectively rationalizable strategy for the agent is deceptive and maximizes the probability of satisfying the task in temporal logic. Such a deceptive strategy is obtained by modeling the opponent’s evolving perception of the agent’s objective and integrating it into planning. This allows the agent to manipulate the opponent’s perception so as to induce the opponent into taking actions that benefit the agent. We demonstrate the effectiveness of our deceptive planning algorithm using robot motion planning examples with temporal logic objectives and design a detection mechanism to notify the agent of potential errors in modeling the adversary’s behavior. Note to Practitioners—Many security and defense applications employ deception mechanisms for strategic advantages. This work presents a game-theoretic framework for planning deceptive strategies in stochastic environments and shows that the opponent modeling plays a key role in the design of effective deception mechanisms. For applications to cyber-physical security, the practitioners can employ temporal logic for specifying security properties in the system and analyze defense with deception using the proposed methods.

In this paper, we propose a sampling-based policy iteration for optimal planning under temporal logic constraints. The method integrates approximate optimal control, importance sampling, and formal methods. For a subclass of linear temporal logic, the planning problem is transformed to an optimal control problem for a hybrid system where discrete transitions are triggered by linear time events in temporal logic. Instead of solving the Hamilton-Jacobi-Bellman equation, we use policy function approximation to reduce the problem into a search of an optimal weight vector that parametrizes the near-optimal policy for given bases. Then, we incorporate Model Reference Adaptive Search - an importance sampling-based optimization algorithm to perform a sample-efficient search within the parameter space of policy function approximations. Facing the discontinuity in cost function introduced by temporal logic constraints and system dynamics, we introduce (1) a rank function in formal logic specifications to enable sample-efficient search; (2) specification-guided basis selection. Under mild technical assumptions, the proposed algorithm converges, with probability one, to a global approximate optimal policy that ensures the satisfaction of temporal logic constraints. The correctness and efficiency of the method are demonstrated through numerical experiments including temporal logic planning for a linear system and a nonlinear mobile robot.