A State Class Construction for Computing the Intersection of Time Petri Nets Languages - LAAS - Laboratoire d'Analyse et d'Architecture des Systèmes Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

A State Class Construction for Computing the Intersection of Time Petri Nets Languages

Résumé

We propose a new method for computing the language intersection of two Time Petri nets (TPN); that is the sequence of labels in timed traces common to the execution of two TPN. Our approach is based on a new product construction between nets and relies on the State Class construction, a widely used method for checking the behaviour of TPN. We prove that this new construct does not add additional expressive power, and yet that it can leads to very concise representation of the result. We have implemented our approach in a new tool, called Twina. We report on some experimental results obtained with this tool and show how to apply our approach on two interesting problems: rst, to dene an equivalent of the twin-plant diagnosability methods for TPN; then as a way to check timed properties without interfering with a system.
Fichier principal
Vignette du fichier
main.pdf (530.94 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-02263832 , version 1 (05-08-2019)

Identifiants

Citer

Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias. A State Class Construction for Computing the Intersection of Time Petri Nets Languages. 17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS), Aug 2019, Amsterdam, Netherlands. ⟨10.1007/978-3-030-29662-9_5⟩. ⟨hal-02263832⟩
67 Consultations
12 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More