Berthomieu et al. [PBV2011] define an extension of TPN with inhibition and permission that provides a method for building composable nets; meaning TPN where all observable transitions have trivial time constraints (their time interval is $[0, \infty[$]). With this extension, it is always possible to build a composable IPTPN from a TPN.
For example, Fig. 1 and 2 below display two TPN and Fig. 3 displays the IPTPN corresponding to their product.
This post describes how to reproduce the experiments reported in our [Formats19] paper. We assume that you already installed Twina and a recent release of Tina. You can also install a Docker image containing all the necessary tools, scripts and model files:
docker pull vertics/twina
In our experiments, we want to compare the results obtained with Product TPN (using Twina) and an encoding into IPTPN. By default, Twina uses option -W, that computes the Linear SCG of a net.
A possible application of our product construction is for model checking TPN, in much the same way some observer-based verification techniques rely on the product of a system with an observer.
The idea is to express a property as the language of an observer, $O$, then check the property on the system $N$ by looking at the behavior of $N \times O$. The product of two nets can be computed with Twina using option -I.
One possible application of Twina, and our initial motivation for this work, is to check the diagnosability of a TPN. We consider a system with a distinguished event that models an unobservable fault (say all transitions with the label $f$). Basically, a system is diagnosable if, when looking only at the observable events and at their timing, we can always detect when an execution contains a fault; and if so after a finite number of observations.