Fundamentos de la Síntesis Reactiva para Especificaciones de Proceso Declarativas

Dada una especificación de Lógica Temporal de Tiempo Lineal interpretada sobre trazas finitas (LTLf), el problema de síntesis reactiva pregunta por encontrar un controlador finitamente representable y terminante que reaccione a las acciones incontrolables de un entorno para hacer cumplir una especificación del sistema deseada. En este artículo estudiamos, por primera vez, los fundamentos de la síntesis reactiva para DECLARE, un lenguaje de modelado de procesos de negocio declarativo y basado en patrones bien establecido, fundamentado en LTLf. Proporcionamos una contribución triple. Primero, definimos un problema de síntesis reactiva para DECLARE. Segundo, mostramos cómo una especificación arbitraria de DECLARE puede ser codificada polinómicamente en una equivalente de tiempo puro-pasado en LTLf, y aprovechamos esto para definir un algoritmo EXPTIME para la síntesis de DECLARE. Tercero, derivamos una versión simbólica de este algoritmo, introduciendo una nueva traducción de fórmulas temporales de tiempo puro-pasado en autómatas finitos deterministas simbólicos.