Step coverability algorithms for communicating systems (Q433351)

This paper develops an extension of the Karp-Miller coverability tree (CT) which is able to characterize the behavior of classes of Petri nets whose semantics is based on concurrent steps instead of occurrences of single transitions. After reviewing the basic algorithm for the CT construction for sequential place/transition Petri nets (PT-nets), the manuscript shows a simple CT extension, the step coverability tree (SCT), that accounts for PT-nets having a step execution semantics, i.e. where concurrently enabled transitions can be fired together in a single step. It is shown that the SCT enjoys similar monotonicity properties as the CT. A notion of maximal step semantics for PT-nets, which is not monotonic, is then considered. For this class of PT-nets it is not possible to build a coverability tree in the general case and the corresponding behavior can be seen as monotonic only in a ``weak'' sense. The paper introduces a class of PT-nets, called ANDMC, modelling acyclic networks of finite state components which communicate by means of buffered channels. ANDMC nets operates under the maximal step semantics and it is demonstrated that for them a suitable coverability tree, the maxSCT, which is able to finitely characterize the reachable markings, can be built. The paper discusses very important issues regarding the analysis and the verification of the behavior of concurrent systems. In particular it extends the applicability of a powerful tool, i.e. the coverability tree, to an important class of communicating systems that can be specified by means of Petri. The manuscript is well written and all the involved concepts are rigorously explained. The only point that could have been improved, in order to make it more readable, is Section 7. Here the class of ANDMC nets is formally defined inductively and the fundamental theorem, based on which their maximal concurrent behavior can be characterized, is proved. A reader could better appreciate the practical applicability of ANDMC if an example of modeling a (simple) communicating system had been included. Also a discussion about the complexity of the algorithm for generating the maxSCT is missing.