Resumen

Presentamos un algoritmo de degeneralización sobre la marcha utilizado para transformar autómatas de Büchi generalizados (GBA) en Autómatas de Büchi (BA) diferentes al algoritmo estándar de degeneralización. La situación contenta, que se utiliza para registrar qué condiciones de aceptación son satisfacibles durante la expansión de fórmulas LTL, se adjunta a los estados y transiciones en el BA. Para obtener el BA determinista, se utiliza la expansión de Shannon de forma recursiva al expandir las fórmulas LTL aplicando las reglas del tableau. El algoritmo de degeneralización sobre la marcha se lleva a cabo en cada paso de la expansión de las fórmulas LTL. Se utilizan diagramas de decisión binaria ordenados para representar el BA y simplificar las fórmulas LTL. Los autómatas temporales se almacenan como gráficos acíclicos dirigidos por sintaxis para ahorrar espacio de almacenamiento. Estas ideas se implementan en un algoritmo de conversión utilizado para construir un autómata de propiedades correspondiente a las

• Materias:Algoritmo de búsqueda Características infrarrojas Retraso difuso Efecto de termoforesis Interpolación
• Subjects:Search algorithm Infrared features Fuzzy delay Thermophoresis effect Interpolation
• Palabras claves:Algoritmo; Desgeneralización; Fórmulas LTL; BA; GBA; Expansión de Shannon
• Keywords:Algorithm; Degeneralization; LTL formulae; BA; GBA; Shannon expansion