Diagnosability of TPN

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.

A simple method to check the diagnosability of a TPN is to adapt the Twin Plant method [SHCK01]. The idea is to build a diagnoser, that is the intersection of two copies of the same system: one with the fault, $N.1$, and another without it, $N.2$, and to check whether we can find an infinite execution with a fault in their intersection. Indeed, if this is the case, then there is an infinite execution after a fault in $N.1$ that can be mistaken with a non-faulty one (in $N.2$). We give an example of this construct in Fig. 1.

In this system, it is not enough to look at the sequence of events: even after a fault, we always observe a $b$ after an $a$. Nonetheless, in the product, every execution where transition $t_4$ fires leads to a time deadlock. Indeed, in this case, we must wait at least 3 (time units) to fire transitions $t_1$ and at most 2 to fire $t_5$ (and both have label $b$). This means that the system is diagnosable. Actually, we detect the occurrence of a fault whenever $b$ does not appear at most 2 (time units) after an $a$.

The twin-plant construction is quite useful and we provide an option to directly build a twin TPN in our tool (with option -twin).

$ twina -fault=f -twin -v -lt faulted.net
# states 3
# transitions 3

class 0
  marking: {p1.1} {p1.2}
  domain:
   2 <= {t2.1} <= 3
   2 <= {t2.2} <= 3
  successors: {t2.1}|{t2.2}:"a"/1

class 1
  marking: {p0.1} {p0.2}
  domain:
   1 <= {t3.1} <= 2
   0 <= {t4.1} <  w
   1 <= {t3.2} <= 2
  successors: {t3.1}|{t3.2}:"b"/0 {t4.1}:"f"/2

class 2
  marking: {p2.1} {p0.2}
  domain:
   3 <= {t1.1} <= 5
   0 <= {t3.2} <= 2
  successors:

In this case, we can generate a LTS for the twin plant and check that every fault eventually leads to a deadlock. For instance using a LTL model-checker and a property such as $(\lozenge f) \Rightarrow (\lozenge \mathrm{deadlock})$.

In the example below we show how to use option -kaut of Twina, in association with option -tina of Ktzio, to generate an output in the KTZ format preserving the labels of the net (option -lt). Then we can use this file with selt, the LTL model-checker provided with Tina.

$ twina -fault=f -twin -kaut -lt faulted.net | ktzio -tina -AUT - faulted.ktz
$ selt -q faulted.ktz -f "(<> f) => (<> dead)"
TRUE

We also provide a dedicated algorithm, option -diag of Twina, to check this property on-the-fly. When the system is not diagnosable, it allows us to find a counter-example before exploring the whole behavior of the twin-plant. Below, we confirm that the net faulted.net is diagnosable; but example basileTAC.net is not. Indeed we find a loop of 6 transitions in the intersection between the net and its twin.

$ twina -fault=f -diag faulted.net

# net is diagnosable
#
# states (explored):   3
# markings:            3
# dbms:                3

$ twina -fault=f -diag -v -lt basileTAC.net
# net is not diagnosable
# length: 6
(*) class 0
  marking: {p0.1} {p0.2}
  domain:
   2 <= {t4.1} <= 2
   1 <= {t5.1} <= 2
   2 <= {t4.2} <= 2
   1 <= {t5.2} <= 2
----[{t4.1}:"i"]--------->
class 1
  marking: {p1.1} {p0.2}
  domain:
   1 <= {t1.1} <= 2
   0 <= {t4.2} <= 0
   0 <= {t5.2} <= 0
----[{t4.2}:"i"]--------->
class 2
  marking: {p1.1} {p1.2}
  domain:
   1 <= {t1.1} <= 2
   1 <= {t1.2} <= 2
----[{t1.1}|{t1.2}:"a" (*)]->
class 3
  marking: {p2.1} {p2.2}
  domain:
   1 <= {t2.1} <= 2
   0 <= {t6.1} <= 2
   1 <= {t2.2} <= 2
   0 <= {t6.2} <= 2
----[{t6.1}:"i"]--------->
class 4
  marking: {p3.1} {p2.2}
  domain:
   1 <= {t7.1} <= 1
   0 <= {t2.2} <= 2
   0 <= {t6.2} <= 2
   {t6.2} - {t2.2} <= 1
----[{t7.1}:"f"]--------->
class 5
  marking: {p4.1} {p2.2}
  domain:
   1 <= {t3.1} <= 2
   0 <= {t2.2} <= 1
   0 <= {t6.2} <= 1
----[{t3.1}|{t2.2}:"b" (*)]->
class 0

Examples used in this post

A basic examples of net with fault from our paper faulted.net

An example from [Basile2015]: basileTAC.net .