Reactive and proactive diagnosis of distributed systems using net unfoldings

We present a diagnosis algorithm for distributed systems modeled as products of transition systems, a model very close to Petri nets. Following the seminal work of Benveniste, Fabre, Haar, and Jard, our algorithm palliates the state-explosion problem by means of the unfolding technique. Given an observation (partial information about a firing sequence), the algorithm constructs a prefix of the unfolding, a compact representation of the executions of the system compatible with the observation. Since the computations of this prefix is algorithmically involved, we define an overap-proximation that trades precision for speed. We report on an implementation that constructs the prefix when the sequence of observations is known (reactive), but also present an online approach, where the diagnosis proactively looks into the future and compare these two approaches. Moreover, we present SAT solving methods for analyzing the explanation.