Dissertação
{en_GB=Multi-robot hybrid motion planning using satisfiability methods} {} EVALUATED
{pt=A automatização de processos é uma necessidade cada vez mais presente na sociedade, principalmente no que toca a exploração espacial. Nesta dissertação são apresentados métodos que permitem o planeamento de uma frota de robôs para a realização de descargas (incluindo arrumação) de carregamentos em micro-gravidade. Para tal, é necessário considerar um modelo híbrido não-linear para o sistema, visto que este apresenta características discretas e continuas em relação ao tempo. Enquanto que a maioria das técnicas existentes se focam em métodos de discretização ou na separação das deliberações continuas e discretas, o trabalho aqui apresentado utiliza autómatos híbridos para representar o sistema, recorrendo posteriormente a uma ferramenta, dReach, que codifica o problema de delta-reachability correspondente em linguagem lógica de modo a que um solver, dReal, consiga encontrar um modelo que valide (solucione) o problema. Assim, a deliberação ocorre tendo em conta ambas as propriedades continuas e discretas do sistema ao mesmo tempo, diferenciando-se das outras técnicas. O uso da ferramenta e solver dReach e dReal permite a consideração das não-linearidades do sistema. Os métodos aqui retratados, inspirados pelos mais recentes avanços nas tecnologias de SMT e também nas ferramentas que aumentam o espectro de problemas que estas podem resolver, servem como prova de conceito evidenciando o potencial destas técnicas para a resolução de problemas de planeamento híbrido em sistemas não lineares, os quais são, historicamente, extremamente complexos de resolver por meios convencionais de planeamento automático., en=Automation is an ever-growing need, especially when it comes to space exploration. In this thesis, the problem of planning for the stowage of cargo by a fleet of robots, in micro-gravity conditions, is tackled. This requires working with a hybrid and non-linear environment, since deliberation on both discrete and continuous-time characteristics of the system have to be made. Most techniques focus on the discretization of the continuous part, or the separation of both discrete and continuous and are not capable of handling non-linearity. The methods presented here consider all of them at the same time by using hybrid automata to describe the system and then, dReach, a tool which encodes the hybrid delta-reachability problem into a logical language, so that a SAT, more specifically SMT solver, dReal, can find a model which validates it (a solution). dReal is the tool which enables taking into account the non-linearity of the system. This work, inspired by the advancements in SMT technology and tools which widen the range of problems they can handle, serves as a proof of concept, showing the potential for the use of the aforementioned techs and tools to solve these types of non-linear hybrid problems, which are historically very complex and hard to solve by conventional planning methods.}
outubro 11, 2021, 11:30
Publicação
Obra sujeita a Direitos de Autor
Orientação
ORIENTADOR
Rodrigo Martins de Matos Ventura
Departamento de Engenharia Electrotécnica e de Computadores (DEEC)
Professor Auxiliar