Negotiating the Probabilistic Satisfaction of Temporal Logic Motion Specifications

TL;DR

This paper presents a control synthesis method for a stochastic vehicle to maximize the probability of satisfying temporal logic specifications, allowing iterative updates and both offline and online applications.

Contribution

It introduces a novel approach combining PCTL specifications with a tree-structured MDP for probabilistic control synthesis, including incremental updates and efficient algorithms.

Findings

Efficient algorithm exploits tree structure for control synthesis.

Specification update rules guarantee satisfaction probability changes.

Method applicable in both offline and online scenarios.

Abstract

We propose a human-supervised control synthesis method for a stochastic Dubins vehicle such that the probability of satisfying a specification given as a formula in a fragment of Probabilistic Computational Tree Logic (PCTL) over a set of environmental properties is maximized. Under some mild assumptions, we construct a finite approximation for the motion of the vehicle in the form of a tree-structured Markov Decision Process (MDP). We introduce an efficient algorithm, which exploits the tree structure of the MDP, for synthesizing a control policy that maximizes the probability of satisfaction. For the proposed PCTL fragment, we define the specification update rules that guarantee the increase (or decrease) of the satisfaction probability. We introduce an incremental algorithm for synthesizing an updated MDP control policy that reuses the initial solution. The initial specification can be updated, using the rules, until the supervisor is satisfied with both the updated specification and the corresponding satisfaction probability. We propose an offline and an online application of this method.