# 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

- see:
- 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).

- see:
- 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)

- see:

## 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