  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.
