13:00
14:00

This talk presents the work I did during my thesis, which I completed in March. Petri nets are a classic formal model for concurrent systems, extensively studied and used since the 1970s. They model fundamental features of concurrent systems such as choice, communication, and process creation. Many subclasses of Petri nets have been defined by forbidding one or more of these features (e.g. marked graphs, free-choice nets, communication-free nets). In our work, we introduce a feature of Petri nets called observation, which is a restricted form of communication. We give a syntactic definition of a class of Petri nets in which the only possible form of synchronization is observation. We study the complexity of analysis problems for this class, called observation Petri nets, and in particular we consider verification problems parameterized by the number of tokens (or processes) in the Petri net. The main analysis problems we study are the class of generalized reachability problems. This class extends reachability queries to possibly infinite sets of markings (or configurations). It includes the cube-reachability problem, which given two sets asks if there is a marking in the first set which can reach a marking in the second set. We show that this class of problems can be decided in polynomial space for observation Petri nets. The classic reachability problem asking if a marking can reach another is also in polynomial space for our observation Petri nets (versus non primitive recursive for general Petri nets). So our results show that it is not harder to check reachability between single markings than it is to check reachability between possibly infinite sets of markings. Thus the observation feature captures a non-trivial property of Petri nets that is particularly interesting for parameterized verification.

salle 178, zoom: https://bordeaux-inp-fr.zoom.us/j/89508306159