Résumé de la diagnosticabilité des motifs dans un réseau de Petri temporisé

MOVEP is a five-day summer school on modelling and verification of parallel processes. It aims to bring together researchers, students, and people from industry working in the fields of control and verification of concurrent and reactive systems. MOVEP seeks to offer a broad spectrum of current research in this area, addressing theoretical and applied aspects of model checking, controller synthesis, software verification, temporal logics, real-time and hybrid systems, stochastic systems, security, run-time verification, etc.International audienceDiagnosability is a basic property of Discrete Event Systems (DES) that relates to the observability of concealed events. Basically, it means that every failure (a distinct instance of unobservable event) can be eventually detected after a nite number of observations. In this work, we are interested by the diagnosability of systems modelled using labelled Time Petri nets (TPN), an extension of Petri nets in which we can associate timing constraints to transitions [6]. This means that we take into account the date at which events are observed and that we want to detect failures in a bounded time. We are also interested by the detection of patterns of events (sequence of observable events that are part of some given regular language) instead of the occurrence of a single fault. The problem of fault diagnosis was introduced by Sampath et al [7] and is well studied in the context of discrete event systems [3,10]. The problem has also been studied on timed models, see for instance the work of Tripakis [8] with Time Automata. In these works, diagnosability is often reduced to properties on the trace language of systems and their composition. These problems are much more dicult when we need to take timing constraints into account. For instance, one of the main problem when considering Time Petri nets is that it is not possible to build the synchronous composition of two transitions when they have non-trivial time constraints. Therefore it is not possible to syntactically dene the intersection of the trace languages of two TPN. We tackle the diagnosability problem using model-checking techniques, which means that we reduce diagnosability to the problem of checking the validity of a temporal logic formula on a nite-state model. This approach relies on a new class of TPN, called Product TPN (PTPN), introduced in [5]. The idea is to enrich TPN with a new synchronization operator (×) that can be used to compute the (language) intersection of two or more TPN