Diagnosis with Petri Net Unfoldings

International audienceLarge distributed system inherently display concurrency, i.e. the fact that several "independent" events may happen in parallel. The more components in a distributed system are independent (or less coupled), the more this feature appears. With its immediate consequence: handling trajectories as sequences of events means representing an explosive number of possible interleavings of concurrent events. To turn independence/concurrency into an advantage rather than an opponent, a key idea is to adopt a true concurrency semantics, that represents runs of a distributed system as partial orders of events. The chapter introduces ways to represent and handle sets of trajectories in such semantics, in particular by means of Petri net unfoldings. It is then explained how one can perform diagnosis with such objects, in the sense of discovering which trajectories of a concurrent system can explain a set of distributed and partially ordered observations. This framework is then extended to the distributed case, where each component aims at building its local view of the diagnosis. Finally, diagnosability issues are examined in the setting of true concurrency semantics, that is the possibility of detecting the occurrence of an unobservable fault not later than after a limited execution following that fault