A Short Overview on Diagnosability of Patterns in Timed Petri Net

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

Éric Lubat (1) , Silvano Dal Zilio (1)

1 LAAS-VERTICS - Équipe Verification de Systèmes Temporisés Critiques

Diagnosability 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.

Domaines: Théorie et langage formel [cs.FL]; Automatique; Algorithme et structure de données [cs.DS]; Systèmes embarqués; Calcul formel [cs.SC]

Éric Lubat, Silvano Dal Zilio. A Short Overview on Diagnosability of Patterns in Timed Petri Net. 14th Summer School on Modelling and Verification of Parallel Processes (MOVEP 2020), Jun 2020, (on line), France. ⟨hal-02899522⟩