Planificación de Trayectorias y Verificación de Modelos

Ponente(s): Everardo Bárcenas .

El problema de planificación de trayectorias consiste en: dados un mapa y conjunto de restricciones, determinar una trayectoria en el mapa que satisfaga las restricciones. Restricciones comunes incluyen un punto inicial en el mapa y la evasión de ciertos puntos (obstáculos). Este problema ha sido tradicionalmente estudiado en el contexto de algoritmos de búsqueda, geométricos y combinatorios. Una de las aplicaciones más conocidas de la planificación de trayectorias es en la construcción de de sistemas de navegación, tales como, automóviles y robots. Por otro lado, la verificación de modelos consiste en determinar si cierta representación abstracta (modelo) de un sistema, que puede ser de software o hardware, satisface determinadas propiedades. Estas propiedades están asociadas al correcto o incorrecto funcionamiento del sistema. Actualmente, las herramientas de verificación de modelos se encuentran en una etapa suficientemente madura como para aplicarse exitosamente a escala industrial. En esta plática se describe el problema de planificación de trayectorias en el contexto de la verificación de modelos en lógicas modales. Estas lógicas fungen como un lenguaje de especificación de restricciones de gran expresividad. La conocida eficiencia de las herramientas de verificación de modelos actuales pueden permitir el cómputo de trayectorias de forma igualmente eficiente.