Formalization of mobile robot tasks

Abstract

The guaranteed coordination and operation of mobile robots without supervision requires tools capable of representing the vast number of evolving possibilities during a mission. This work studies the categorical and logical formalization of mobile robot tasks, with the use of connections between robotics, distributed computing and modal logics. A demonstration of the equivalences between modal logics and combinatorial topology is shown as the first element for the unified perspective, alongside some of its uses. This is followed by a discussion on the connections between models in distributed computing and robotics, where initial results on the formalization of robot tasks are accompanied by considerations on applications for gathering and exploration missions. The work ends by proposing a formalization that extends the previous one in the literature with the capacity of dealing with faulty robots, limited sensing capabilities and uncertain behavior.

A coordenação e operação de robôs sem supervisão requere ferramentas capazes de representar o vasto número de possíveis evoluções de uma missão. Este trabalho é um estudo da formalização categórica e lógica de tarefas de robôs móveis, fazendo uso de conexões entre robótica, computação distribuída e lógica modal. Uma demonstração da equivalências entre lógica modal e topologia combinatória é exibida como o primeiro elemento de uma perspectiva unificada, junto dos seus usos. Uma discussão segue com as conexões entre modelos em computação distribuída e robótica, onde resultados iniciais na formalização de tarefas de robôs são acompanhados por considerações nas seus usos para missões de encontro e exploração. Este trabalho encerra com a proposta de uma formalização que extende a anterior encontrada na literatura com a capacidade de lidar com robôs defeituosos, capacidades limitadas de sensoriamento e comportamento incerto.