Checking Properties with Language Intersection

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.

A major advantage of this approach is that there is no risk to disrupt the system under observation, which is not always easy to prove with other methods. We give an example of observer in Fig. 1.

In this net, sequences of events $a$ and $b$ may occur in any order and at any date. On the other hand, the only way to fire $t_5$ is to “find” two successive occurrences of $a$ and $b$ with a delay (strictly) bigger than 2. Hence we can check if such behavior is possible in a system, $N$, by checking whether transition $t_5$ can fire in $N \times O$.

For instance, we can use this observer on the net basileTAC.net with the following command.

$ twina -I -aut basileTAC.net observer.net
des(0,20,12)
(0,"t4.1",1)
(0,"t5.1",2)
(1,"t1.1|t1.2",2)
(1,"t1.1|t4.2",5)
(2,"t2.1|t0.2",0)
(2,"t6.1",3)
(3,"t7.1",4)
(4,"t3.1|t0.2",0)
(5,"t2.1|t2.2",0)
(5,"t6.1",6)
(6,"t7.1",7)
(7,"t3.1|t2.2",0)
(7,"t3.1|t5.2",8)
(8,"t4.1",9)
(8,"t5.1",10)
(9,"t1.1|t3.2",2)
(10,"t2.1|t2.2",0)
(10,"t2.1|t5.2",8)
(10,"t6.1",11)
(11,"t7.1",7)

We find two states where transition $t_5$ could fire in the observer (that is transition {t5.2} in the result); one synchronized with transitions $t_3$ of the net, the other with $t_2$. If we change the timing constraints in the observer, we still find examples with the constraint $[5, \infty[$ but none with $]5, \infty[$. Hence we know that the maximal possible duration between event $a$ and $b$ in model basileTAC is exactly 5.

Examples used in this post

A basic examples of observer observer.net , also in graphical format observer.ndr (for display and editing with nd).

An example from [Basile2015]: basileTAC.net .