Síntesis Basada en Flujo de Pruebas Reactivas para Sistemas de Toma de Decisiones Discretas con Especificaciones de Lógica Temporal

Diseñar pruebas para evaluar si un sistema autónomo dado satisface especificaciones complejas es un desafío debido a la complejidad de estos sistemas. Este trabajo propone un enfoque basado en flujo para la síntesis de pruebas reactivas a partir de especificaciones de lógica temporal, permitiendo la síntesis de entornos de prueba que consisten en obstáculos estáticos y reactivos y agentes de prueba dinámicos. Las especificaciones de lógica temporal describen el comportamiento de prueba deseado, incluyendo los requisitos del sistema así como un objetivo de prueba que no se revela al sistema. La estrategia de prueba sintetizada impone restricciones sobre las acciones del sistema en reacción al estado del sistema. Las pruebas son mínimamente restrictivas y logran el objetivo de la prueba mientras garantizan la realizabilidad del objetivo del sistema sin ayudarlo (configuración semi-cooperativa). Se aprovechan la teoría de autómatas y las redes de flujo para formular un programa lineal entero mixto (MILP) para sintetizar la estrategia de prueba. Para un agente de prueba dinámico, la estrategia del agente se sintetiza para una especificación GR(1) construida a partir de la solución del MILP. Si la especificación no es realizable por la dinámica del agente de prueba, se utiliza un enfoque guiado por contraejemplos para resolver el MILP hasta que se encuentre una estrategia. Esta síntesis de prueba reactiva basada en flujo se lleva a cabo fuera de línea y es agnóstica al controlador del sistema. Finalmente, la estrategia de prueba resultante se demuestra en simulación y experimentalmente en un par de robots cuadrúpedos para una variedad de especificaciones.