On the composition of time Petri nets (Q645045): Difference between revisions

The design and verification of concurrent and distributed systems, especially when their dynamic behaviour is time-dependent, is an intrinsically hard problem. One of conceptually elegant and efficient ways of dealing with this problem is to use a modular, or compositional, construction of such systems. Moreover, one also requires that the behaviour of a composite system can be derived from the behaviours of its components. Petri nets are a fundamental model of concurrent and distributed systems, and time Petri nets (TPN) allow one to express timing constrains of potential activities providing an adequate modelling framework for real time systems. In general, Petri nets support a compositional approach thanks to parallel composition and transition synchronisation. However, in presence of time, the method for assembling components based on transition synchronisation is not always compositional. Motivated by this observation, the paper addresses the following specific question: how to construct a concurrent system in a compositional manner from components specified by TPNs? This, in turn, leads to another question: given a TPN component, how can one transform it into an equivalent model where synchronised transitions are not time-dependent? The solution proposed in this paper is based on a new class of TPNs called forbid/allow TPNs (faTPNs). The ``forbid'' relation is similar to the priority relation, whereas the ``allow'' relation is in a way an inverse of priority. The class of faTPNs is then investigated and its general applicability discussed.