A CTL model repair method for Petri Nets

Computation Tree Logic (CTL) model repair is a modern, formal tool that allows the verification and modification of models, by generating new admissible models that represent the correct design of systems. In concurrent and distributed systems modeling, due to the difficulty of expressing those behaviors in transitions systems, is suitable using Petri nets as specification formalism. In this paper we present a CTL model repair methodology for models specified as Petri nets; it consists of semantics of CTL formulae, a set of basic repair operations, and a general repair algorithm for modifying Petri nets models. The method is illustrated through an example dealing with a double redundant system.