Section: New Results

Contextual Petri nets

Contextual nets (c-nets) are an extension of Petri nets that – unlike ordinary Petri nets – faithfully models concurrent read accesses to shared resources. This is not only interesting from a semantic but also from an algorithmic point of view, as the analysis of such nets can better exploit the fact that concurrent reads are independent and concurrent. In particular, the unfolding of a contextual net may be up to exponentially smaller in certain situations.

In previous work carried out in the Mexico project, we established theoretical foundations [6] and efficient algorithms for constructing c-net unfoldings [42] . More recently, we have investigated verification techniques based on c-nets. These exploit the advantages mentioned above to obtain results more efficiently. The results have been published in the Concur 2012 conference [70] . In parallel, the development of the Cunf tool has continued, see 5.1.2 . We are currently exploring how the technique can be combined with that of merged processes [107] for further speed-ups, and its applications in diagnosis.