Redes de Petri, algoritmo para la construcción de árboles de mínima cobertura

Abstract

En el ámbito del diseño de sistemas embebidos críticos, donde predominan las reacciones a eventos y la lógica basada en acciones, las Redes de Petri emergen como una herramienta de modelado esencial. Mediante la implementación de una ecuación de estado extendida, es posible capturar la lógica de estos sistemas. El modelo lógico resultante se ejecuta a través de un monitor que integra la lógica (Red de Petri), la política (gestión de conflictos) y las acciones, formando un sistema heterogéneo. Esta integración mejora la capacidad del sistema para ser verificado mediante formalismos matemáticos basados en el modelo empleado. En este contexto, la verificación de propiedades importantes de las RdP, como la cobertura, la acotación, la alcanzabilidad y la vivacidad, se realiza utilizando árboles de cobertura, con un tiempo de verificación proporcional al tamaño del árbol. Por lo tanto, es crucial diseñar algoritmos que calculen el árbol de cobertura de manera eficiente. En este trabajo, presentamos una modificación del algoritmo de árbol de cobertura mínima, originalmente propuesto por Karp y Miller. Para hacer este cálculo, se memorizan las aceleraciones activándolas como transiciones ordinarias. Esta estrategia no solo asegura un límite predecible para el uso de memoria adicional —específicamente, un máximo de doble exponencial—, sino que también mejora la eficiencia operativa. La implementación de un prototipo de este algoritmo muestra su competitividad, presentando un uso reducido de memoria y tiempos de ejecución comparables a las herramientas más rápidas disponibles.