Éric Lubat, Silvano Dal Zilio, Didier Le Botlan, Yannick Pencolé, Audine Subias
In FORMATS 2019 — 17th International Conference on Formal Modeling and Analysis of Timed Systems, aug 2019.
PDF DOI〈10.1007/978-3-030-29662-9_5〉 HAL-02263832
Abstract#
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 lead 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: first, to define an equivalent of the twin-plant diagnosability methods for TPN; then as a way to check timed properties without interfering with a system.
Citation#
@InProceedings{DalzilioS:formats2019twina,
author = {Lubat, Éric and {Dal Zilio}, Silvano and {Le Botlan}, Didier and Pencolé, Yannick and Subias, Audine},
title = {{A State Class Construction for Computing the Intersection of Time Petri Nets Languages}},
booktitle = {FORMATS 2019 -- 17th International Conference on Formal Modeling and Analysis of Timed Systems},
series = {Lecture Notes in Computer Science},
volume = {11750},
publisher = {Springer-Verlag},
doi = {10.1007/978-3-030-29662-9_5},
pages = {79--95},
month = aug,
year = 2019
}