Verificación de extensiones de Redes de Petri con precios, tiempo y múltiples instancias

Resumen

Las redes de Petri son un lenguaje formal adecuado para la modelización y verificación de sistemas concurrentes con infinitos estados. Sin embargo, en muchas ocasiones las redes de Petri carecen de la expresividad necesaria para representar características de los sistemas que se manejan, como el manejo de tiempo y costes reales, o la presencia de varios procesos con un número no acotado de estados ejecutándose en paralelo. En la literatura se han definido algunas extensiones para la representación de las características anteriores. Por ejemplo, las ¿Redes de Petri con Tiempo¿ con manejo de tiempo real y las nu-redes de Petri (nu-PN), capaces de representar un número no acotado de procesos con infinitos estados. En esta tesis definimos varias extensiones que reúnen estas dos características y estudiamos sus propiedades de decidibilidad. En primer lugar definimos las ¿nu-Redes de Petri con Tiempo¿, capaces de representar sistemas con un número no acotado de procesos, donde cada proceso es representado por un nombre diferente, y un número no acotado de relojes reales. En este modelo un reloj de un proceso debe satisfacer ciertas condiciones para formar parte en el disparo de una transición. Desafortunadamente, probamos que la verificación de propiedades de seguridad es indecidible para este modelo, incluso en el caso con solo dos relojes por proceso. Por esto, definimos las "nu-PN Localmente Síncronas¿ (nu-lsPN), que manejan un solo reloj por proceso y probamos que la verificación de propiedades de seguridad es decidible. Además, estudiamos la expresividad de las nu-lsPN, demostrando que son la extensión de las redes de Petri no Turing-completa más expresiva. Una vez encontrado un formalismo apropiado para la modelización de sistemas con tiempo, nos disponemos a definir un nuevo modelo con tiempo y costes extendiendo las nu-lsPN, considerando dos tipos de coste: los costes de disparo, producidos por la ejecución de acciones, y los costes de almacenamiento, producidos por el almacenamiento de recursos durante el paso del tiempo. Así, definimos el problema de seguridad siguiente: dado un presupuesto b, decimos que un sistema es seguro si no podemos cubrir un conjunto de estados dado gastando más de b. De nuevo, obtenemos un resultado positivo para la decidibilidad de esta propiedad. Por último, aplicamos los resultados anteriores en la verificación de propiedades de seguridad y corrección para flujos de trabajo con tiempo y costes en las que varios procesos son ejecutados concurrentemente, compartiendo recursos globales. Antes de definir los nuevos modelos, ampliamos los resultados ya existentes sobre flujos de trabajo restringidos por los recursos (rcwf,), considerando una definición de corrección algo más general que la ya existente. Entonces, definimos dos modelos de rcwf con tiempo y precios: en el primer modelo suponemos que el tiempo pasa durante las ejecuciones de acciones y en el segundo el tiempo pasa entre las diferentes ejecuciones de acciones, y por lo tanto los costes de almacenamiento se producen entre estas. Así, podemos calcular el coste de un proceso en una ejecución sumando los costes de disparo y almacenamiento producidos por el proceso. Dado que en cada ejecución participan múltiples procesos, podemos calcular el coste global de la ejecución de diferentes formas: consideramos la suma, el máximo, la media, y la suma ponderada de los precios de los procesos. Así, decimos que una red es segura si el precio global de ninguna ejecución válida supera el presupuesto dado. Finalmente, obtenemos que la seguridad es decidible para la suma, el máximo, la media y la suma ponderada finita en el primer modelo, y el máximo y la suma ponderada finita en el segundo modelo. Respecto a la corrección, demostramos que esta es decidible para rcwf con tiempo y precios cuya seguridad es decidible bajo algunas hipótesis adicionales.