Las líneas de productos de redes de Petri (PNPL) proporcionan un formalismo potente y compacto para modelar y analizar la variabilidad del comportamiento en sistemas concurrentes. Al permitir anotaciones basadas en características sobre transiciones, lugares y arcos, PNPL permite la especificación unificada de múltiples variantes de productos en un único modelo del 150% de redes de Petri. Sin embargo, la comprobación de propiedades dinámicas como la alcanzabilidad, la ausencia de bloqueo y la vivacidad en todas las configuraciones sigue siendo un reto importante. Las técnicas tradicionales de comprobación de modelos no suelen ser escalables o carecen de soporte para una semántica que tenga en cuenta la variabilidad. La lógica CTL (del inglés, Computational Tree Logic) con características (fCTL) se ha introducido para razonar formalmente sobre propiedades de comportamiento en Líneas de Producto de Software (SPL) modeladas utilizando Sistemas de Transición con características (FTS+). Mientras que fCTL es muy adecuado para la comprobación de modelos basados en características, su aplicación a modelos PNPL no se ha explorado sistemáticamente.
En este trabajo investigamos la aplicabilidad e idoneidad de fCTL para PNPL proponiendo un proceso de transformación estructurado de PNPL a FTS+ a través de un gráfico de alcanzabilidad anotado por características. Nuestro enfoque consta de tres pasos principales: (i) Construir un RG anotado por características a partir del modelo PNPL, preservando explícitamente la información de variabilidad de la red original;
(ii) Convertir este RG en una representación FTS+ correspondiente mediante la definición de mapeos formales para estados, transiciones, guardias de características y proposiciones atómicas;
(iii) Aplicar especificaciones fCTL al FTS+ resultante para verificar propiedades como la alcanzabilidad, la libertad de bloqueo y la vivacidad a través de configuraciones de características válidas.
Con tal fin, evaluamos nuestra metodología a través de casos de estudio ilustrativos, incluyendo modelos PNPL representativos con comportamiento multi-token y restricciones de características complejas. Nuestros resultados experimentales muestran que el enfoque propuesto captura eficientemente la variabilidad tanto estructural como de comportamiento de PNPL a la vez que permite una verificación escalable basada en fCTL. La transformación también admite estrategias de poda de características para eliminar configuraciones no válidas causadas por la convergencia de múltiples características.
Este trabajo demuestra la viabilidad de unir PNPL y fCTL a través de un modelo de comportamiento intermedio que preserva las características. Aporta una vía formal y práctica para aplicar la verificación lógica temporal en sistemas concurrentes configurables, ofreciendo una perspectiva novedosa para el análisis formal de líneas de productos de sistemas.
–ABSTRACT–
Petri Net Product Lines (PNPL) provide a powerful and compact formalism for modelling and analysing behavioural variability in concurrent systems. By allowing feature-based annotations on transitions, places, and arcs, PNPL enables the unified specification of multiple product variants in a single 150% Petri net model. However, verifying dynamic properties such as reachability, deadlock-freedom, and liveness across all configurations remains a significant challenge. Featured Computation Tree Logic (fCTL), an extension of Computation Tree Logic (CTL), has been introduced to formally reason about behavioural properties in Software Product Lines (SPLs) modelled using Featured Transition Systems (FTS+). While fCTL is well-suited for feature-aware model checking, its application to PNPL models has not been systematically explored.
In this work, we investigate the applicability and suitability of fCTL to PNPL by proposing a structured transformation pipeline from PNPL to FTS+ through an feature-annotated Reachability Graph. Our approach involves three main steps:
(i) Constructing a feature-annotated RG from the PNPL model, explicitly preserving variability information from the original net;
(ii) Converting this RG into a corresponding FTS+ representation by defining formal mappings for states, transitions, feature guards, and atomic propositions;
(iii) Applying fCTL specifications to the resulting FTS+ for verifying properties such as reachability, deadlock-freedom, and liveness across valid feature configurations.
We evaluate our methodology through illustrative case studies, including representative PNPL models with multi-token behaviour and complex feature constraints. Our experimental results show that the proposed approach efficiently captures both the behavioural and structural variability of PNPL while enabling scalable fCTL-based verification. The transformation also supports feature pruning strategies to eliminate invalid configurations caused by multiple-feature convergence.
This work demonstrates the feasibility of bridging PNPL and fCTL through an intermediate feature-preserving behavioural model. It contributes a formal and practical pathway for applying temporal logic verification in configurable concurrent systems, offering a novel perspective for the formal analysis of system product lines.
Las líneas de productos de redes de Petri (PNPL) proporcionan un formalismo potente y compacto para modelar y analizar la variabilidad del comportamiento en sistemas concurrentes. Al permitir anotaciones basadas en características sobre transiciones, lugares y arcos, PNPL permite la especificación unificada de múltiples variantes de productos en un único modelo del 150% de redes de Petri. Sin embargo, la comprobación de propiedades dinámicas como la alcanzabilidad, la ausencia de bloqueo y la vivacidad en todas las configuraciones sigue siendo un reto importante. Las técnicas tradicionales de comprobación de modelos no suelen ser escalables o carecen de soporte para una semántica que tenga en cuenta la variabilidad. La lógica CTL (del inglés, Computational Tree Logic) con características (fCTL) se ha introducido para razonar formalmente sobre propiedades de comportamiento en Líneas de Producto de Software (SPL) modeladas utilizando Sistemas de Transición con características (FTS+). Mientras que fCTL es muy adecuado para la comprobación de modelos basados en características, su aplicación a modelos PNPL no se ha explorado sistemáticamente.
En este trabajo investigamos la aplicabilidad e idoneidad de fCTL para PNPL proponiendo un proceso de transformación estructurado de PNPL a FTS+ a través de un gráfico de alcanzabilidad anotado por características. Nuestro enfoque consta de tres pasos principales: (i) Construir un RG anotado por características a partir del modelo PNPL, preservando explícitamente la información de variabilidad de la red original;
(ii) Convertir este RG en una representación FTS+ correspondiente mediante la definición de mapeos formales para estados, transiciones, guardias de características y proposiciones atómicas;
(iii) Aplicar especificaciones fCTL al FTS+ resultante para verificar propiedades como la alcanzabilidad, la libertad de bloqueo y la vivacidad a través de configuraciones de características válidas.
Con tal fin, evaluamos nuestra metodología a través de casos de estudio ilustrativos, incluyendo modelos PNPL representativos con comportamiento multi-token y restricciones de características complejas. Nuestros resultados experimentales muestran que el enfoque propuesto captura eficientemente la variabilidad tanto estructural como de comportamiento de PNPL a la vez que permite una verificación escalable basada en fCTL. La transformación también admite estrategias de poda de características para eliminar configuraciones no válidas causadas por la convergencia de múltiples características.
Este trabajo demuestra la viabilidad de unir PNPL y fCTL a través de un modelo de comportamiento intermedio que preserva las características. Aporta una vía formal y práctica para aplicar la verificación lógica temporal en sistemas concurrentes configurables, ofreciendo una perspectiva novedosa para el análisis formal de líneas de productos de sistemas.
–ABSTRACT–
Petri Net Product Lines (PNPL) provide a powerful and compact formalism for modelling and analysing behavioural variability in concurrent systems. By allowing feature-based annotations on transitions, places, and arcs, PNPL enables the unified specification of multiple product variants in a single 150% Petri net model. However, verifying dynamic properties such as reachability, deadlock-freedom, and liveness across all configurations remains a significant challenge. Featured Computation Tree Logic (fCTL), an extension of Computation Tree Logic (CTL), has been introduced to formally reason about behavioural properties in Software Product Lines (SPLs) modelled using Featured Transition Systems (FTS+). While fCTL is well-suited for feature-aware model checking, its application to PNPL models has not been systematically explored.
In this work, we investigate the applicability and suitability of fCTL to PNPL by proposing a structured transformation pipeline from PNPL to FTS+ through an feature-annotated Reachability Graph. Our approach involves three main steps:
(i) Constructing a feature-annotated RG from the PNPL model, explicitly preserving variability information from the original net;
(ii) Converting this RG into a corresponding FTS+ representation by defining formal mappings for states, transitions, feature guards, and atomic propositions;
(iii) Applying fCTL specifications to the resulting FTS+ for verifying properties such as reachability, deadlock-freedom, and liveness across valid feature configurations.
We evaluate our methodology through illustrative case studies, including representative PNPL models with multi-token behaviour and complex feature constraints. Our experimental results show that the proposed approach efficiently captures both the behavioural and structural variability of PNPL while enabling scalable fCTL-based verification. The transformation also supports feature pruning strategies to eliminate invalid configurations caused by multiple-feature convergence.
This work demonstrates the feasibility of bridging PNPL and fCTL through an intermediate feature-preserving behavioural model. It contributes a formal and practical pathway for applying temporal logic verification in configurable concurrent systems, offering a novel perspective for the formal analysis of system product lines. Read More
Related posts:
Ingeo Túneles 9
Estudio de los parámetros operativos de una sembradora neumática a chorrillo para la dosificación variable basada en un mapa de prescripción
Accuracy Comparison of CNN, LSTM, and Transformer for Activity Recognition Using IMU and Visual Markers
Estimación del ángulo de giro óptimo en seguidores solares de un eje horizontal con paneles bifaciales mediante algoritmos de inteligencia artificial
Utilización de los sistemas de información geográfica para la estimación automática de la escorrentía directa
Análisis de la variabilidad de una placa de 316L fabricada por DED mediante el uso de Small Punch