Analysis issues in Petri nets with inhibitor arcs

We investigate the problem of extending the analysis techniques developed for P/T systems to a proper subclass of P/T systems with inhibitor arcs. We start proposing an extension of the coverability tree construction to a subclass of P/T systems with inhibitor arcs, whose elements will be called henceforth primitive systems. We show that the coverability tree corresponding to a primitive system is finite and is a good representation of its behaviour; hence, it can be used as an analysis tool to check properties such as place boundedness, the existence of dead transitions and of a reachable marking larger than a given one. Then we provide an encoding of primitive systems in P/T systems, which permits to retrieve the firing sequences of the primitive system from the firing sequences of the corresponding P/T system. The close correspondence between the firing sequences of the two systems is used prove the decidability of reachability, deadlock and liveness for primitive systems. We also obtain that the model checking problem for the linear time mu-calculus and labelled primitive systems is decidable. We show that primitive systems coincide with the largest class of P/T systems with inhibitor arcs whose transition sequences can be simulated by a standard P/T system; we also show that in general the step behaviour of a primitive system cannot be simulated by any P/T system. These results are then used to investigate the expressiveness of inhibitor arcs regarding the class of generated languages. (C) 2002 Elsevier Science B.V. All rights reserved.