Algebras of coloured Petri nets

These are Petri net based formalisms equipped with operators like those typically found in process algebras. By enriching Petri nets with additional labelling, it becomes possible to define these operators as Petri nets compositions or transformations. As a consequence, an important difference with process algebras is that the expected behaviour is obtained by a statical arrangement of the Petri nets instead of by a dynamical enforcement through the semantics. In other words, if the additional labelling is discarded, we just use regular Petri nets and any existing tool for Petri nets can be used to analyse the obtained models.

Numerous variants of such algebras of Petri nets have been defined over years, forming a rich family that was recently unified through a consistent presentation in my habilitation thesis (also published as a book available for purchase at Amazon or MoreBooks!). This forms a modular framework including varied modelling features: control flow, synchronous and asynchronous communication, exceptions, threads, functions and time.

Efficient model-checking

Using structured modelling formalisms like algebras of Petri nets yields models whose structures exhibit peculiarities introduced by the formalism. This can often be exploited to improve the performance of model-checking the corresponding models. So, while developing modelling features within the algebras of Petri nets, I keep concerned with these verification issues and correspondingly develop efficient model-checking procedures. Until now, parallel computation of the state space, reduction and approximation techniques, as well as optimised compilation of the models have been considered.

Application domains

Applications form both the motivation and the destination of my research work. On the one hand, a new application domain provides the motivation to introduce new modelling features or develop efficient verification techniques. On the other hand, applying the so developed theory allows to validate it on concrete use cases. After having been involved with safety related applications, in particular in time-constrained systems, I'm now more considering applications in the fields of security protocols and systems biology.

Tools and implementation

Most of the formalisms I develop have been implemented (or are currently being implemented) within the SNAKES toolkit. This work allows both to actually run the considered applications, but also it generally leads to simplify the theoretical definitions: implementing things is an opportunity to reconsider them from another point of view, allowing to find simplifications, generalisations or better formulations.