Planificación de trayectorias basada en verificación de modelos

Abstract

El presente documento muestra una nueva perspectiva al aborda el problema de la Planificación de Trayectorias, que consiste en la generación de una trayectoria, lo que es una ruta de un punto A a un punto B con ciertas restricciones. En la actualidad existen diferentes maneras de solucionar este, regularmente lo que buscan es la ruta o trayectoria más corta entre un punto y otro punto, pero no son capaces de seguir rutas cumpliendo ciertas especificaciones, lo cual se cumple con el enfoque propuesto de la Verificación de Modelos. La Verificación de Modelos es un método en el que teniendo una estructura matemática relacional, se verifica si una fórmula lógica satisface una estructura para ser un modelo de la fórmula. Gracias a esta verificación se tiene la capacidad de contemplar variables dentro de la estructura y casos secuenciales que pueden darse dentro de esta, por ello su uso principal ha sido identificar errores dentro de los sistemas. Esta capacidad de describir un sistema para verificar posibles casos, plantea nuevas especificaciones como tener obstáculos o lograr un orden de pasos que ocurren en el sistema, por ello emplear este procedimiento permite verificar el cumplimiento de especificaciones para una ruta. En esta tesis se muestra el acercamiento de la Verificación de Modelos para obtener trayectorias, donde mediante premisas se obtiene una conclusión o ruta. Estas premisas son determinadas por el lenguaje lógico de las lógicas modales, en específico el de la lógica temporal. Las lógicas modales con su complejidad computacional y poder de expresividad son capaces de especificar diversas restricciones, como lo es la espacialidad y la temporalidad, con ello se obtienen rutas que cumplen especificaciones más flexibles o estrictas a las actualmente usadas, por lo que logran dar nuevas aplicaciones a la Planificación de Trayectorias. Además, en el presente documento se muestra la aplicación de la Verificación de Modelos, con el desarrollo de un prototipo funcional de la Planificación de Trayectorias en un navegador de propósito general, usando un mapa con puntos a través del API de Google Maps para generar la estructura relacional, que dada una fórmula en CTL y su traducción al verificador NuSMV, entrega una ruta con especificaciones dadas por un usuario, con lo que se expone una aplicación a una situación cotidiana para planear una visita a Ciudad Universitaria.