En esta Tesis Doctoral se aborda el problema de la modelización
y la verificación de sistemas concurrentes sujetos a cambios
dinámicos.
El formalismo de base es el de las redes de Petri. En lo que concierne
a la expresividad del modelo se busca un mecanismo que tenga en
cuenta los cambios dinámicos estructurales de manera local, interna
e incremental. Al mismo tiempo, las propiedades básicas de las redes
de Petri (acotabilidad de lugares, alcanzabilidad, interbloqueo y vivacidad)
deben continuar siendo decidibles para este modelo extendido.
En general, lo que se gana normalmente en términos de expresividad
se traduce en una pérdida en términos de propiedades decidibles.
Hay que buscar, entonces, un equilibrio entre expresividad y computabilidad.
Las
gramáticas de grafos y las
redes automodificantes de
Valk son las dos líneas de investigación origen de nuestro
modelo
general: los
sistemas de reescritura de redes. Ambas líneas
dan lugar a modelos que mejoran la expresividad de las redes de Petri
para describir el cambio dinámico en sistemas concurrentes pero
tienen el inconveniente de que casi todas las propiedades básicas
decidibles
de las redes de Petri se pierden. Por ello, para estos modelos extendidos
no pueden construirse herramientas automáticas de verificación.
Los
sistemas de reescritura de redes son una combinación
de redes de Petri con sistemas de reescritura de grafos. Cada configuración
del sistema es una red de Petri y un cambio de configuración es
una regla de reescritura de grafos. La expresividad de los sistemas de
reescritura de redes es la misma que la de la máquina de Turing,
es decir, las propiedades básicas decidibles de las redes de Petri
se pierden
en estos sistemas, no siendo posible la verificación automática.
Las
redes reconfigurables son una subclase de los sistemas de reescritura
de redes equivalente formalmente a las redes de Petri, lo que
asegura que todas las propiedades fundamentales de las redes de Petri siguen
siendo decibibles para este modelo y, por tanto, es
factible la verificación automática.