Towards verifying Petri Nets: a model cheking approach

Abstract

Las redes de Petri son un importante formalismo para la especificación de sistemas concurrentes y distribuídos. Tal y como se hace con otros formalismos, como los autómatas finitos, nos gustaría poder verificar formal y automáticamente ciertas propiedades sobre los sistemas representados mediante redes de Petri. Este problema se denomina "model checking" (o comprobación de modelos). En este trabajo hemos hecho una recopilación de los principales resultados sobre model checking para redes de Petri y dos de sus principales extensiones monótonas que son ortogonales: las redes reset y las ν-PNs. Comenzamos con una pequeña introducción a las redes de Petri, sus extensiones y los principales resultados de decidibilidad sobre estas, que sirven para demostrar cuestiones sobre model checking. Una de las principales tareas realizadas en este trabajo ha sido identicar resultados sobre model checking para otros formalismos y adaptarlos a las extensiones de redes de Petri anteriormente citadas. A pesar de la naturaleza eminentemente bibliográfica del trabajo, presentamos también algunos resultados originales. En particular, se da una demostración de la indecidibilidad del recubrimiento repetido para ν-PNs y de aquí se deduce la indecidibilidad del problema de model-checking para cierta lógica temporal para ν-Petri nets. Finalmente, al encontrarnos con que todas las lógicas temporales consideradas son indecidibles para las redes reset y las ν- PNs, discutimos cómo enfrentarnos al problema del model checking en el caso indecidible, mediante dos técnicas diferentes: el unfolding y el cómputo del cover. [ABSTRACT] Petri nets are an important formalism to specify concurrent and distributed systems. When Petri nets are used to model systems, we would like to be able to verify certain properties about the modelled systems automatically, as is done when other formalisms, as nite automata, are applied. This problem is called the "model checking" problem. In this work, we present a compilation of the main model checking results for plain Petri nets and two orthogonal monotonic extensions: reset Petri nets and ν-Petri nets. We rst introduce Petri nets and its extensions, and summarize the main decidability results for them, which are useful in proving decidability issues about model checking. An important part of the work has been looking for model checking results about other formalisms (in particular lossy VASS with inhibitor arcs) which are applicable to reset nets and ν-Petri nets. Despite the fact that this work is eminently bibliographic, some new results are proved here. In particular, a proof for the undecidability of the repeated coverability problem for ν-Petri nets is given, and we use this result to prove the undecidability of model checking certain temporal logic for ν-Petri nets. Finally, as all the considered temporal logics for reset nets and ν-Petri nets are undecidable, we discuss how to approach the model checking problem in the undecidable case with two different techniques: unfolding and cover computation.