Robust Temporal Logic Planning Under Contingency Constraints

In dynamic and uncertain environments, robots are often required not only to complete their primary tasks but also to be able to switch to a contingency mode that facilitates a safe and effective response in the face of an unpredictable event. In this paper, we address the problem of synthesizing optimal high-level control policies for a robot 1) to satisfy a desired task and 2) to be able to respond safely in the face of an unexpected event. We model the dynamics of the robot as a Stochastic Transition System. We express the primary task as a Time Window Temporal Logic (TWTL) specification, and we consider the contingency behavior to be reaching a safe region in at most k time steps with a probability greater than a desired threshold. We propose an automata-theoretic framework to compute optimal policies for task satisfaction and contingency behavior. While the contingency behavior is always ensured, the task satisfaction probability is maintained by minimally extending the mission horizon when necessary. We demonstrate the performance of the proposed method through simulations and experiments.