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