Probabilistic Analysis Applied to Cleaning Robots

Abstract

Robots are increasingly being used in industry and starting their way in our homes as well, particularly cleaning robots. The common techniques to analyze cleaning robots are based on simulations or statistical experiments made from filming robots' movements. In this work, we propose an alternative way of performing such an analysis by using Probabilistic Model Checking with the language and tool PRISM. We propose a PRISM characterization for robot motion algorithms that can be used as the input for simulations as well as check exhaustively whether an algorithm satisfies specific Probabilistic Temporal formulas. The proposed PRISM model allows measuring energy consumption and time to complete missions; such metrics are helpful to compare different algorithms considering specific environments. Furthermore, to ease the use of our work, we hide the PRISM syntax by proposing an imperative style DSL used to specify the algorithms. We illustrate those ideas with motion planning algorithms for home cleaning robots.