Control of Noisy Differential-Drive Vehicles from Time-Bounded Temporal Logic Specifications

TL;DR

This paper presents a method for controlling noisy differential-drive robots to maximize the probability of satisfying complex temporal logic specifications, using Markov decision processes and statistical model checking, with simulations and experiments validating the approach.

Contribution

It introduces a novel control strategy that maps noisy robot measurements to an MDP and computes policies to optimize specification satisfaction probability.

Findings

The control policy effectively increases the likelihood of satisfying BLTL specifications.

Simulation and experimental results demonstrate the approach's practical viability.

The method provides a probabilistic guarantee on specification satisfaction in noisy environments.

Abstract

We address the problem of controlling a noisy differential drive mobile robot such that the probability of satisfying a specification given as a Bounded Linear Temporal Logic (BLTL) formula over a set of properties at the regions in the environment is maximized. We assume that the vehicle can determine its precise initial position in a known map of the environment. However, inspired by practical limitations, we assume that the vehicle is equipped with noisy actuators and, during its motion in the environment, it can only measure the angular velocity of its wheels using limited accuracy incremental encoders. Assuming the duration of the motion is finite, we map the measurements to a Markov Decision Process (MDP). We use recent results in Statistical Model Checking (SMC) to obtain an MDP control policy that maximizes the probability of satisfaction. We translate this policy to a vehicle feedback control strategy and show that the probability that the vehicle satisfies the specification in the environment is bounded from below by the probability of satisfying the specification on the MDP. We illustrate our method with simulations and experimental results.