Use Cases and Benchmarks

This post is used to collect most of the models used in our experiments, with a reference to the original paper where they appear when possible.

Examples of TPN (from the Tina distribution)

• Alternating Bit Protocol abp.net
• IFIP example taken from [Berthomieu83]: ifip.net
• Level-crossing example with 3 trains: train3.net

Intersection of TPN

• The two basic examples used in our [Formats19] paper: C1.net and C2.net

Diagnosability with the Twin-Plant Method and IPTPN

• A timed version of the example in [DEDS17]: jdedstimed.net
  • see: Diagnosability analysis of patterns on bounded labeled prioritized Petri nets, Gougam, HE., Pencolé, Y. & Subias, A. Discrete Event Dyn Syst (2017) 27: 143
  • the same example in graphical format , for viewing with Tina’s nd program
• An example from [Basile2015]: basileTAC.net .
  • see: State estimation and fault diagnosis of labeled time petri net systems with unobservable transitions. Basile, F., Cabasino, M. P., & Seatzu, C. (2015). IEEE Transactions on Automatic Control, 60(4).
• An example from [Wang2015]: wangTAC.net .
  • see: Diagnosis of time Petri nets using fault diagnosis graph. Wang, X., Mahulea, C., & Silva, M. (2015). IEEE Transactions on Automatic Control, 60(9)

Diagnosability of Patterns and Single-Fault

• An example of pattern (a total, deterministic TPN) for the property three consecutive occurrences of $F1$ without $F2$: omega.net
• A timed version of the product transportation system found in [DEDS17]: transport_timed.net ; see transport.ndr for a graphical version of the original (untimed) model