=Paper=
{{Paper
|id=Vol-1846/paper8
|storemode=property
|title=Coloured Petri Nets Based Diagnosis on Causal Models
|pdfUrl=https://ceur-ws.org/Vol-1846/paper8.pdf
|volume=Vol-1846
|authors=Soumia Mancer,Hammadi Bennoui
|dblpUrl=https://dblp.org/rec/conf/apn/MancerB17
}}
==Coloured Petri Nets Based Diagnosis on Causal Models==
https://ceur-ws.org/Vol-1846/paper8.pdf
Coloured Petri Nets Based Diagnosis on Causal
Models
Soumia Mancer and Hammadi Bennoui
Computer science department, LINFI Lab.
University of Biskra, Algeria
mancer.soumia@gmail.com, bennoui@gmail.com
Abstract. In the last decades, several approaches have been proposed
in order to capture the problem of causal model-based diagnosis within
Petri Nets (PNs) framework, where both the structural and behavioural
analysis of the net model are exploited for reasoning. In fact, PNs are
a useful tool, but most of the approaches suffer from the large size of
the obtained models even for simple systems. This paper introduces a
novel class of Coloured Petri Nets (CPNs) called Causal CPNs. Such
a net model is motivated by representing the causal behaviour of the
system to be diagnosed, as well as, simplifying the analysis methods.
The diagnosis technique exploits backwardly the reachability graph of
the net model. A case study is used to illustrate the usefulness of our
proposal for fault diagnosis.
Keywords: model-based diagnosis, causal models, coloured Petri nets,
reachability graphs
1 Introduction
Model-based approach as an alternative to heuristic based one, especially when
the experimentations are missing, deals widely with fault diagnosis in such a
manner that the examination of a given system is done on the basis of a model. It
aims at explaining any observed behaviour that conflicts with the way the system
is meant to behave. Among the diagnosis frameworks found in the literature,
those based on causal models where the explanations would be given in terms
of initial causes leading the system to a misbehaviour.
In logical frameworks, a causal model-based diagnosis problem is traditionally
solved through symbolic manipulations that are shown as a cumbersome task;
and hence, numerous attempts to face this problem have been done. In partic-
ular, Petri nets (PNs) have been used to represent the causal model, and so to
exploit their analysis techniques to implement efficiently the diagnosis reason-
ing mechanisms [1, 2]. For problems where the net model is large or composed
of some identical parts, it is well known that Coloured PNs (CPNs) are well
suited to use with respect to classical PNs. By means of data type primitives,
it is possible to achieve a reduced model about the behaviour of the system
under examination. The manipulation of the data values carried by tokens that
124 PNSE’17 – Petri Nets and Software Engineering
reside in places of a CPN model is done through the arc expressions. Generally,
those expressions are functions that define the added/removed tokens to/from a
place. Nevertheless, when analysing the CPN model backwardly, those expres-
sions may exhibit a more complicated process because of the inversion task. In
order to simplify this latter, and so, the analysis phase, we propose resorting to
matrices as a way of manipulating the token colours in the net model.
In this paper, we focus on the use of CPNs for causal model-based diagnosis.
For that reason, we introduce a particular CPN called Causal-CPN (CCPN)
that allows representing the causal behaviour of the system to be diagnosed by
means of causal matrices that are attached to transitions of the net model. Causal
matrices are used to define the possible inputs and their associated outputs of
transitions as causal relationships. For solving a given diagnosis problem based
on CCPN, a backward analysis on the corresponding markings graph is defined
in this paper to generate the possible diagnoses. In fact, such analysis can be
seen as the coloured version of the BW-analysis that has been proposed in [2]
for some simplified Petri nets called Behavioural Petri Nets.
The present paper starts in section 2 by outlining briefly some basic defini-
tions on which we will rely throughout the paper. Section 3 introduces the CCPN
model by which it is possible to restrict CPNs for representing causal models. A
formalisation of the model-based diagnosis problem by means of CCPNs is de-
tailed in section 4, and solving such a problem is shown in section 5 by exploiting
the backward reachability analysis on reachable markings graph. Finally, section
7 concludes the paper and outlines future work.
2 Preliminaries
In this section, we outline some basic definitions that we need in this paper.
2.1 Causal model
From [1], a causal model is a couple (V, E) where V is a set of entities, noted
states, and E is a set of cause-effect relationships among states. For the diagnosis
reason, states are classified into Initial-causes, Internal states and Manifestations.
The states of a causal model are used to represent the states (partial states) of
the modelled system. Initial causes represent initial states from which any evo-
lution in the system begins. Internal states describe the unobservable part of the
system as consequences of initial states. Manifestations represent the observable
states of the system as consequences of internal states. Each of the states can
be instantiated by assigning a value to it from a finite and predefined set noted
admissible_values. It is important to keep in mind that each state must assume
at most one value at a given time and it can be present on the model or absent.
2.2 diagnosis problem
A diagnosis problem is defined logically in [3] as a triple DP = (BM, IN IT, <
Ψ + , Ψ − >) where BM is the behavioral model of the system to be diagnosed,
Mancer et.al.: Coloured Petri Nets Based Diagnosis on Causal Models 125
IN IT is the set of instances of initial causes in terms of which the obser-
vations have to be explained, Ψ + is a subset of observations to be entailed
by a solution of DP and Ψ − is the set of all possible values that conflict
with the made observation (that are known to be absent in the case under
examination). Let OBS be the current set of observations, thus, Ψ + ⊆ OBS
and Ψ − = {m(x)|m(y) ∈ OBS, x 6= y} such that m is a manifestation and
x, y ∈ admissible_values(m). A solution to DP is a set ∆ ⊆ IN IT such that
∆ predicts each parameter in Ψ + and no parameter in Ψ − :
∀x ∈ Ψ + BM ∪ ∆ ` x
∀y ∈ Ψ − BM ∪ ∆ 0 y
Where ` is the derivation symbol.
2.3 Coloured Petri nets
Coloured Petri Nets [4] are high-level nets merging both Petri Nets and the
functional programming language Standard ML in one model. CPNs still retain,
as strong points of PNs, the foundation of the graphical notation and the basic
primitives for modelling concurrency, communication and synchronisation, while
Standard ML provides the primitives for data types definition and data values
manipulation.
As CPNs are basically PNs, it is important to keep in mind that a CPN
model is defined by a finite set of places, a finite set of transitions and a finite
set of arcs as connections between places and transitions. Each place has an
associated type and may hold one or more tokens each of which carries a data
value belonging to the place’s type. By convention, types are colour sets thus,
tokens are token colours.
Each place has its own marking which is a multiset of token colours that
are present in such a place. The sum of individual place markings gives the
marking of the CPN model. The marking changes during the execution of the
model by means of transition’s firing. As it is known, when a transition occurs
it removes tokens from its input places and it adds tokens to its output places.
In CPN, the removed (resp. added) tokens are determined by an arc expression
associated to the outgoing (resp. incoming) arc from (resp. to) a place. An arc
expression is built from typed variables, constants, operators, and functions and
it evaluates to a multi-set of token colours. Moreover, it can be attached to each
transition a boolean expression (with variables) called a guard which specifies
the bindings for which it evaluates to true. A binding is an assignment of data
values to the free variables appearing in the expression of an incoming arc or
a guard of a transition. A binding of a transition can be written in the form:
(v1 = d1 , v2 = d2 , ..., vn = dn ) where f or i ∈ 1..n : vi is a variable and di is the
value assigned to vi .
A transition t is enabled, ready to occur, if there is a binding such that:
1) the evaluation result of each of the input arc expressions is present on the
corresponding input place; and 2) the guard (if any) is satisfied. The firing of a
126 PNSE’17 – Petri Nets and Software Engineering
t adds to each output place a multi-set of token colours to which the expression
on the corresponding output arc is evaluated.
Before recalling the formal definition of a CPN from [4], we recall the concept
of multi-sets. A multiset is a set where individual elements may occur more than
once.
Definition 1. (Multi set) A multisetPm, over a non-empty set S, is a function
m ∈ [S → N] represented formally by: s∈S m(s)0 s.
• ∀s ∈ S : s ∈ m iff m(s) 6= 0.
• SM S is set of all finite multi-sets over S.
A set of operations that can be applied on multisets are defined as follows:
∀m, m1 , m2 ∈ SM S and ∀n ∈ N:
P
|m| = Ps∈S m(s).
m1 + m2 = s∈S (m1 (s) + m2 (s))0 s.
m1 6= m2 = ∃s ∈ S : m1 (s) 6= m2 (s).
m1 6 m2 = ∀s ∈ S : m1 (s) 6 m2 (s)
(defined analogously for >).
Thus, a CPN is given by:
Definition 2. A Coloured Petri net (CPN) is a 6-tuple N = (Σ, P, T, A, C, G)
where:
• Σ is a non-empty set of types (colour sets).
• P is a non-empty set of places.
• T is a non-empty set of transitions.
• P ∩ T = ∅, P ∪ T 6= ∅.
• A is a non-empty set of arcs such that: A ⊆ (P × T ) ∪ (T × P ).
• C : P → Σ is a colour function maps each place into a colour set.
• G is a guard function maps each transition into a boolean expression.
Definition 3. A marked CPN is a pair (N, µ) where N is a CPN and µ is a
function defined on P such that:
µ(p) ∈ C(p)M S , ∀p ∈ P.
3 Causal-Coloured Petri nets
CPNs are used for representing and analysing a large variety of systems. The
colour set concept allows us to obtain a reduced net model. While through the
expressions associated with transitions (guards) or the arcs we define the possible
combinations of input and output token colours for a transition to fire, and so,
describing the evolution of the system under study. All the analysis techniques
defined for classical PNs are extended for CPNs. Among them, we are interested
in backward ones. The backward analysis of a CPN seems as an inversion of
Mancer et.al.: Coloured Petri Nets Based Diagnosis on Causal Models 127
the net model [5] and hence realising the analysis forwardly. The main problem
that arises, here, is the backfiring of a transition. When inverting the arcs, their
expressions have to be inverted too, and the same as the transition’s guard.
Such an inversion depends on the input and the output arc expressions of the
transition. It may lead to a combinatorial explosion in some cases. In order to face
this problem, we propose associating with each transition a matrix describing
the possible combinations of input and output token colours. As a result, the
expressions of the input arcs of a transition are typed variables and the output
ones are simple expressions that extract from a given matrix and according to the
input tokens the possible output ones. In the following, we introduce a particular
class of CPNs called Causal CPNs characterised by matrices associated with their
transitions. CCPNs are used to represent the causal behaviour of the system
under examination.
Definition 4. A Causal-Coloured Petri Net is a 6-tuple N = (Σ, P, T, A, C, F W )
where:
• (Σ, P, T, A, C) is a CPN.
• P = Ic ] Is ] M n:
Ic = {p|p ∈ P, • p = ∅}1 , M n ⊆ {p|p ∈ P, p• = ∅} while Is = P \ (Ic ∪
M n).
• A+ , denotes the transitive
S closure of A, is irreflexive.
• F W : T −→ M ATn,m ( ω∈Σ ω)2 such that:
◦ n is the number of transitions for which a transition t may be unfolded
in a classical PN (i.e, it is the number of ways that t may fire.)
◦ m = |• t|+|t• | defines the number of places connected with t, either inputs
or outputs.
Definition 5. A marked CCPN is a pair (N, µ) where N is a CCPN and µ is
a marking such that:
∀p ∈ P : |µ(p)| 6 1.
Let µ0 be the initial marking of N such that: ∀p ∈ P : µ0 (p) 6= ∅ → p ∈ Ic.
Definition 6. A marked CCPN (N, µ0 ) is said to be safe iff:
∀p ∈ P, ∀µ ∈ R(N, µ0 ) : |µ(p)| 6 1.
Where R(N, µ0 ) denotes the reachability set from µ0 .
Let us introduce the following notations for the rest of the paper.
Note 1. ∀t ∈ T and ∀(x1 , x2 ) ∈ A:
– A(t) denotes the set of the input arcs of t.
1 •
x = {y|(y, x) ∈ A} and x• = {y|(x, y) ∈ A} denote the input and output sets of x
2 S x ∈ P ∪ T.
respec. where
M ATn,m ( ω∈Σ ω) defines the space of matrices of n lines and m colomns.
128 PNSE’17 – Petri Nets and Software Engineering
– V ar(t) denotes the set of variables that appear in the input arc expressions of
t and in its associated guard G(t) (it is also used for expressions V ar(expr)).
In a CCPN model: V ar(G(t)) = V ar(t).
– E(x1 , x2 ) denotes the expression attached to an arc (x1 , x2 ).
Definition 7. A binding of a transition t is a function b defined on V ar(t) such
that:
- ∀v ∈ V ar(t) : b(v) ∈ T ype(v).
- Let V ar(t) = {v1 , ..., vn }: [b(v1 ) b(v2 ) ... b(vn )] be the ith sub-vector-line of
F W (t).
Expr < b > denotes the evaluation of the expression Expr in the binding b.
As a particularity of CCPN, in comparison with CPN, is the irreflexivity
of A+ ; hence, the CCPN model is acyclic. Thus, it is possible to introduce a
partial order, noted ≺, between its transitions. Such an order is inspired from
that which is defined for BPNs in [2] as follows:
Let t1 , t2 ∈ T : t1 ≺ t2 ⇔ t1 A+ t2 .
Definition 8. Let µ be a marking, a transition t is enabled at µ iff:
∀p ∈ • t : E(p, t) < b > 6 µ(p) and @t0 ≺ t s.t t0 is enabled.
Definition 9. Let t be an enabled transition in a marking µ, the firing of t
changes the marking µ to anothor marking µ0 as follows:
∀p ∈ P : µ0 (p) = µ(p) − E(p, t) < b > +E(t, p) < b > .
Definition 10. Given a marked CCPN (N, µ), we denote by a step the set of
enabled and concurrent transitions at µ.
Definition 11. Given a marked CCPN (N, µ) and a stepSs = {t1 , .., tn }, the
n
firing of s at µ reaches the new marking µ0 such that µ0 = i=1 µi , µ[ti > µi .
In a CCPN model, places are used to represent the entities of the causal
model of the system to be diagnosed. As we have mentioned, it suffices to dis-
tinguish, for diagnosis purposes, among three classes of entities: Initial causes,
noted Ic, represented by source places, Internal states, noted Is, represented by
places that have input transitions, and Manifestations, noted M n, represented by
sink places. Transitions represent the cause-effect relations among correspond-
ing places. To each transition is attached a matrix given by F W (t) for which its
lines represent the different ways that such a transition t can fire while each of
its columns is associated with a place p that surrounds t, and so, it determines
the possible values that will be consumed/produced from/in p by the firing of t.
Each transition matrix F W (t) can be divided into two sub-matrices F W _in(t)
and F W _out(t). F W _in corresponds to the possible combining token colour
Mancer et.al.: Coloured Petri Nets Based Diagnosis on Causal Models 129
inputs of t while F W _out is the output sub-matrix of t. Furthermore, each tran-
sition t can be classified as joint or fork transition, it is noticed that the linear
transition is a particular fork or joint transition. A joint transition is used, as
usual, to represent a conjunction of places, but also, it is used, in a CCPN, to
deal with both cases where there are several concurrent possibilities for reach-
ing a place or where there is an exclusive-or between, at least, two execution
paths for reaching that place. As the marking of a place and the evaluation
of an arc expression is a multiset, we inspire the idea of exploiting the empty
sets as components of a joint transition matrix to describe the mentioned cases
above for better and more logical representation of the system behaviour. In the
case where there are several concurrent evolutions starting from a place by the
same value, a fork transition will be used to duplicate the required place by the
specified marking for each path. For each transition t, the input arc expressions
are typed variables while the output arc expression is a function that holds as
inputs a binding vector and the transition matrix and returns the output token
colour that corresponds to such a binding. The net model is safe, that is, any
place must be marked by, at most, one token colour.
Definition 12. Let (N, µ) be a marked CCPN, the marking µ may lead to an
inconsistency iff: ∃ti , tj ∈ T, ∃µi , µj ∈ R(N, µ) :
µ[ti > µi ∧ µ[tj > µj ∧ ∃p ∈ P |µi (p) 6= µj (p).
Example 1. As an example of a CCPN model, we consider a simple model
adapted from an example given in [1] which is used to represent a partial fault
model of a car engine. However, it is representative enough for introducing the
basic constructs of CCPNs. Fig.1 gives the graphical representation of the con-
sidered model. Such a model is characterized by c1 , c2 and c3 as initial-causes of
the described causal model, and m1 and m2 as manifestations. The left places
represent the internal states. Each place has a type, attached to it, which de-
termines the set of colours that the token on the place is allowed to have. As a
sample, the tokens residing in c1 will have an a or b as their token colour.
The transitions are used to model the cause-effect relationships among the
corresponding entities in the causal model. Each transition is labelled by a matrix
that defines its firing ways. t1 is a fork transition that is used to duplicate the
input place c1 by the marking a into c11 and c12 by the same token color. In
F W (t1 ), the first column corresponds to the input place c1 , while, the last two
ones correspond to the output places c11 and c12 . t2 will be enabled only if one
of the input places is marked by the colour a, and as a result, it produces an
a or b colour in s1 . The transition t3 is as the logical and while t5 and t8 are
as the logical or. The transition t8 can be enabled in three cases (according to
the number of lines in its matrix), the two first ones represent the case when
either s3 or s4 is marked by a color a while the last is that when both places are
marked by such a color. The transition t5 has the same interpretation as t8 , but
only, with t8 the produced color is the same for all the cases (firing ways), and
so, it is used to guard the safeness of the model (each place is marked at most by
one color at a given time), while with t5 the produced color is defined according
130 PNSE’17 – Petri Nets and Software Engineering
𝑐1 𝑎, 𝑏
𝑎 𝑎 𝑎 𝑡1
𝑎, 𝑏 𝑎, 𝑏
𝑐3 3 𝑐11
𝑎 𝑎 𝑡2
𝑎 𝑏
𝑎, 𝑏, 𝑐 𝑎, 𝑏 𝑎, 𝑏, 𝑒
𝑠1 𝑐12 𝑐2 2
𝑡7 𝑎 𝑎 𝑏 𝑎 𝑡6 𝑡3 𝑎 𝑎 𝑎
𝑎 𝑏 𝑏
𝑎, 𝑒 𝑎, 𝑏, 𝑑
𝑠3 𝑠4 𝑠2 𝑎, 𝑏, 𝑐
𝑎 𝑎 𝑡8 𝑡5 𝑡4
𝑏 𝑓 𝑎 𝑐
𝑎 𝑎
𝑎 𝑎 𝑎 𝑏 𝑑
𝑎, 𝑏 𝑏 𝑏 𝑒 𝑎, 𝑐, 𝑑, 𝑒, 𝑓
𝑚2 𝑚1
Fig. 1. A CCPN example.
to the presence of colors in s2 and s4 , and here, t5 guards the consistency of the
net model.
4 Formalising diagnosis with CCPNs
CCPNs, as particular CPNs for representing the causal behaviour of a system,
are introduced mainly to deal with fault diagnosis. In this section, we show how
the diagnosis problem that is given in Definition 2.2 can be formalised in the
basis of a CCPN model. A diagnosis problem is pointed out when it appears a
discrepancy between the required behaviour of the examined system and its real
one. In causal model-based diagnosis, the observed behaviour is given as a set
of manifestations, noted OBS. In CCPNs, it consists of a final marking µOBS
where the marked places are those belonging to M n. Formally, it is given by:
Definition 13. Given a CCPN as a model of the system S, an observation is a
marking µOBS such that:
∀p ∈ P : µOBS (p) 6= ∅ → p ∈ M n.
Definition 14. A diagnosis problem is defined in terms of a CCPN model by
the triple: DP = (N, IN IT, < M + , M − >) where:
– N is the CCPN model.
– IN IT = {(p, c)|p ∈ Ic, c ∈ C(p)}.
Mancer et.al.: Coloured Petri Nets Based Diagnosis on Causal Models 131
– M + = {(p, c)|p ∈ M n, c ∈ C(p), µOBS (p) = c}.
– M − = {(p, c)|p ∈ M n, c ∈ C(p), µOBS (p) 6= c}.
In this definition, N represents the causal behavioural model of the system
to be diagnosed. IN IT is a set of couples (p, c) in terms of which diagnosis so-
lutions would be given. It consists of a set of possible markings c of each place
p that represents an initial cause in the causal model. < M + , M − > represents
the made observation. M + consists of a set of couples (p, c) representing mani-
festations that have to be entailed by a solution to DP , while M − is the set of
couples (p0 , c0 ) that conflict with the made observation (i.e, it is used to ensure
the required consistency).
Definition 15. Let N be a CCPN, p ∈ P , c ∈ C(p) and µ0 an initial marking;
(N, µ0 ) ` (p, c) ↔ ∃µ ∈ R(N, µ0 )|µ(p) = c.
While,
(N, µ0 ) 0 (p, c) ↔ ∀µ ∈ R(N, µ0 )|µ(p) 6= c.
Definition 16. Let N be a CCPN, p ∈ P , c ∈ C(p) and µ0 an initial marking;
A generalization of Definition 15 for a set Q = {(p, c)|p ∈ P, c ∈ C(p)} is given
by:
(N, µ0 ) ` Q ↔ ∃µ ∈ R(N, µ0 )|∀(p, c) ∈ Q : µ(p) = c.
While,
(N, µ0 ) 0 Q ↔ ∀µ ∈ R(N, µ0 )|∀(p, c) ∈ Q : µ(p) 6= c.
The notion of diagnosis solution can be now captured by the following propo-
sition.
Proposition 1. Given a diagnosis problem DP = (N, IN IT, < M + , M − >),
an initial marking µ0 is a solution to DP iff:
(N, µ0 ) ` M + and (N, µ0 ) 0 M − .
This means that µ0 has to account for all observations in M + , while, no one in
M − must be reached from µ0 .
Proof. We proceed to prove this proposition by contradiction.
(→)
Suppose that µ0 is a solution to DP and that [(N, µ0 ) ` M + ∧(N, µ0 ) 0 M − ]
does not hold.
By Definition 16: (∀µ ∈ R(N, µ0 )∃(p, c) ∈ M + : µ(p) 6= c) ∨ (∃µ ∈
R(N, µ0 )∃(p, c) ∈ M − : µ(p) = c).
And so, µ0 is not a solution, which contradicts with our first assumption.
(←)
Suppose that [(N, µ0 ) ` M + ∧ (N, µ0 ) 0 M − ] and that µ0 is not a solution.
By Definition 16: (∃µ ∈ R(N, µ0 )|∀(p, c) ∈ M + : µ(p) = c) ∧ (∀µ ∈
R(N, µ0 )|∀(p, c) ∈ M − : µ(p) 6= c).
As a result, µ0 is a solution, which is a contradiction.
t
u
132 PNSE’17 – Petri Nets and Software Engineering
5 diagnosis problem solving with CCPNs
In order to solve a diagnosis problem given by means of a CCPN, we are inter-
ested in the backward reachability analysis. In this section, a formalisation of
the method is given for analysing a CCPN model, and so, generating a set of
possible diagnoses that explain a given malfunction.
Generally, a backward analysis on reachability graphs allows determining the
markings from which a given marking is reachable. It can be done by a simple
direction inversion of the arcs in classical PNs, while, the transition’s firing rule
remains the same as forwarding one. When dealing with CPNs, the inversion
has to be applied on arc expressions and transition guards that are, generally,
functions. For linear transitions, the inversion process is trivial. For the case of a
fork or joint transitions, the inversion process becomes complicated. Thus, it is
possible to fall in a combinatorial explosion problems. In a CCPNs, in addition
to direction inversion of the arcs, the inversion process can be achieved simply
by a re-ordering of the transition matrices F W . In such a way, the input sub-
matrix F W _in becomes output, denoted b_F W _out. While, the output sub-
matrix F W _out becomes input, denoted b_F W _in. As a result, F W becomes
b_F W . And so, arc expressions have to be changed. As usual, each input arc
expression of a transition t is a typed variable; while, each output one equals
to the following expression f ([vq1 ..vqm ], b_F W (t))(p) such that, p is added to
specify which place is (i.e, f ([vq1 ..vqm ], b_F W (t)) is a vector, for which, each of
its components corresponds, backwardly, to an output place).
Definition 17. Let M be a marking, a transition t is backwardly enabled in M
iff:
∀p ∈ t• : E(t, p) < b > 6 M (p) and @t0 t.
Such that t0 is backwardly enabled and the binding b is defined over b_F W (t).
Assuming that a transition t is backwardly enabled, the backfiring of t makes
the execution process of the model returning back, where it removes token colors
{ci }1≤i≤n from the output places of t and adds a set of others {c0j }1≤j≤m each of
which to its own place that belongs to the input ones of t. This set of colours can
be easily defined by the backward transition matrix of t. By the same manner
as forwarding one, the new marking µ0 can be calculated from µ after firing the
transition t. Furthermore, µ may lead to an inconsistent marking (Definition 12).
A marking µ is an inconsistent one for the case when there is a fork transition t
in which its output places have different markings other than the empty set.
Definition 18. Let (N, µ) be a marked CCPN, µ is said to be inconsistent iff:
∃t ∈ T, ∃p, p0 ∈ t• : µ(p) 6= µ(p0 ).
Definition 19. Given a marked CCPN (N, µ), let t be a fork transition such
that • t = {p} and t• = {p1 , ..., pm }, t is forced backwardly at the marking µ iff:
• t is not backwardly enabled at µ.
Mancer et.al.: Coloured Petri Nets Based Diagnosis on Causal Models 133
• ∃pi (1 ≤ i ≤ m)|µ(pi ) 6= ∅.
• µ is not inconsistent.
• @t0 t where t0 is backwardly enabled or forced at µ.
If t is forced at µ then ∀p, p0 ∈ t• such that µ(p) = ∅ and µ(p0 ) 6= ∅, consider
µ(p) = µ(p0 ).
Solving a diagnosis problem given by DP consists of constructing backwardly
a reachability graph. We start such a construction from a submarking µ of µOBS
such that ∀(p, c) ∈ M + : µ(p) = c, while the others are empty. The terminal
nodes of the graph can be initial markings ranged in a set µini , inconsistent
markings or markings leading to an inconsistency. The arcs of the graph are
labelled by steps (It should be noted that, in this case, a step is a set of back-
wardly enabled transitions at the given marking). The set of initial markings
µini is a set of markings µi in such a manner that µ is a submarking of µ0 where
µ0 ∈ R(N, µi ). The set µini represents the candidate solutions to the given prob-
lem, thus, a consistent solution is a candidate marking that does not, by any
way, lead to any combination in M − . To ensure that, we build for each marking
of µini the corresponding forward reachability graph. We select as consistent
solutions the markings that reach no element of M − .
Example 2. In order to show how diagnoses are computed, we consider the
example depicted in Fig. 1 with an observation given by the marking µOBS ,
where µOBS (m1 ) = c and µOBS (m2 ) = a (For simplicity, we use the notation
of sets in which the elements are couples of places with its markings, and so:
µOBS = {(m1 , c), (m2 , a)}). A classification of those observed manifestations can
be that in which M + = µOBS . According to the classification of the observed
manifestations, the diagnosis problem definition will be given as it has been dis-
cussed in [3], where the authors suggest that for the same observation, we may
have a spectrum of definitions varying from a pure consistency-based to a pure
abductive diagnosis. Fig. 2 shows the backward reachability graph corresponding
to the case that we have where µ = µOBS . Arcs of the graph are labelled by steps
(the set of fired transitions in backward fashion). The framed transitions rep-
resent forced ones. Notice that t1 is forced when the place c12 becomes marked
with a color a (that is present in b_F W (t1 )). Moreover, there is a path in the
backward reachability graph whose terminal node is an inconsistent marking
where the place s1 has two different markings.
The obtained solutions are µ1 = {(c1 , a), (c2 , a)} and µ2 = {(c1 , a), (c2 , a),
(c3 , a)}. It should be noticed that µ1 ⊂ µ2 , thus, µini = {µ1 } (a solution to a
diagnosis problem have to be minimal). For our case, µ1 is a consistent solution.
6 Related work
During the last decade, several model-based approaches and frameworks have
been proposed, as improved ones, to solve fault diagnosis problem. The major-
ity of them perform such a reasoning on the basis of PNs and their different
134 PNSE’17 – Petri Nets and Software Engineering
{(𝑚1 , 𝑐), (𝑚2 , 𝑎)}
𝑡4 , 𝑡8 𝑡4 , 𝑡8
𝑡4 , 𝑡8
{(𝑠2 , 𝑎), (𝑠4 , 𝑎)}
{(𝑠2 , 𝑎), 𝑠3 , 𝑎 , (𝑠4 , 𝑎)}
{(𝑠2 , 𝑎), (𝑠3 , 𝑎)}
𝑡3 , 𝑡6
𝑡3 , 𝑡7
{(𝑐12 , 𝑎), 𝑐2 , 𝑎 , (𝑠1 , b)} 𝑡3 , 𝑡6 , 𝑡7
{(𝑐12 , 𝑎), 𝑐2 , 𝑎 , (𝑠1 , 𝑎)} 𝑡2 {(𝑐12 , 𝑎), 𝑐2 , 𝑎 , (𝑠1 , 𝑎), (𝑠1 , b)}
𝑡2 Inconsistent
{(𝑐12 , 𝑎), 𝑐2 , 𝑎 , (𝑐11 , 𝑎)}
{(𝑐12 , 𝑎), 𝑐2 , 𝑎 , (𝑐3 , 𝑎)} 𝑡1
𝑡1 {(𝑐1 , 𝑎), (𝑐2 , 𝑎)}
{(𝑐1 , 𝑎), 𝑐2 , 𝑎 , (𝑐3 , 𝑎)}
Fig. 2. A backward reachability graph.
extensions as suitable formalisms because of their mathematical and graphical
representation. Among the recent works, we recall those proposed in the context
of discrete event systems. The approach proposed in [6] exploits basis markings
for an on-line diagnosis using labelled PNs. The main advantage of such an ap-
proach is that the reachability space is more compact. In the field of CPNs, [7]
presents a CPN version of the diagnoser introduced in [8]. It should be known
that such a diagnoser is constructed on the basis of a labelled PN model of
the diagnosed system. The approach is, then, extended to implement a modular
diagnoser for distributed and large systems. [9] deals with the problem of diag-
nosis in workflow processes, where, the author defines a CPN fault model, in
which the faults can be of two sources: faulty input places or faulty transition
modes. Places represent the system variables that can be of a correct, faulty or
unknown status. The diagnosis problem reasoning is accomplished backwardly
by solving its corresponding symbolic inequations system. The authors of [5]
develop a backward reachability analysis method for CPNs. Such a method per-
forms a structural inversion 3 of the CPN model, and so, analysing the CPN
model backwardly becomes a forward analysis of its inverted one.
3
Such an inversion preserves the original model proprieties.
Mancer et.al.: Coloured Petri Nets Based Diagnosis on Causal Models 135
Our proposal differs from these by focusing on a particular side, when mod-
elling a system, that is the causal behaviour. In this scope, we are interested in
the approach presented in [2] for centralised diagnosis performed on the basis of
BPNs, and its corresponding distributed one defined in [10]. CCPNs are defined
as a particular and simplified class of CPNs for describing the causal behaviour,
as well as, simplifying the analysis methods.
7 Conclusion
In this paper, we have presented a new approach based on CCPNs as a particular
class of CPNs for representing and diagnosing systems given by means of causal
models. In such a net model, we introduced for each of its transitions a matrix
describing the functional dependencies among its corresponding places as a way
of avoiding the hard problems resulting from the inversion of the arc expressions
when analysing the net model backwardly. In order to solve a diagnosis problem
given by means of CCPNs, and so, generating the possible diagnoses of a given
malfunction, a backward analysis on the reachability graph corresponding to the
net model is defined for the case when using matrices. Many issues remain to
be investigated. Among those we mention: the use of structural analysis as an
alternative of reachability graphs that are characterized by the combinatorial
explosion during the consistency checking of the generated initial markings; and
extending the approach for the distributed systems where there is a set of sub-
systems each of which is given by a CCPN having its local observation and so
local diagnoses, the main question is that how can interactions be managed to
achieve global consistency between the different local diagnoses.
References
1. L. Portinale, “Verification of causal models using petri nets,” International Journal
of Intelligent Systems, vol. 7, no. 8, pp. 715–742, 1992.
2. ——, “Behavioral petri nets: a model for diagnostic knowledge representation and
reasoning,” IEEE Transactions on Systems, Man, and Cybernetics, Part B (Cy-
bernetics), vol. 27, no. 2, pp. 184–195, 1997.
3. L. Console and P. Torasso, “A spectrum of logical definitions of model-based diag-
nosis,” Computational intelligence, vol. 7, no. 3, pp. 133–141, 1991.
4. K. Jensen, “Coloured petri nets and the invariant-method,” Theoretical computer
science, vol. 14, no. 3, pp. 317–336, 1981.
5. M. Bouali, P. Barger, and W. Schon, “Colored petri net inversion for backward
reachability analysis,” IFAC Proceedings Volumes, vol. 42, no. 5, pp. 227–232, 2009.
6. M. P. Cabasino, A. Giua, M. Pocci, and C. Seatzu, “Discrete event diagnosis using
labeled petri nets. an application to manufacturing systems,” Control Engineering
Practice, vol. 19, no. 9, pp. 989–1001, 2011.
7. Y. Pencolé, R. Pichard, and P. Fernbach, “Modular fault diagnosis in discrete-event
systems with a cpn diagnoser,” IFAC-PapersOnLine, vol. 48, no. 21, pp. 470–475,
2015.
136 PNSE’17 – Petri Nets and Software Engineering
8. M. Sampath, R. Sengupta, S. Lafortune, K. Sinnamohideen, and D. Teneketzis,
“Diagnosability of discrete-event systems,” IEEE Transactions on automatic con-
trol, vol. 40, no. 9, pp. 1555–1575, 1995.
9. Y. Li, “Diagnosis of large software systems based on colored petri nets,” Ph.D.
dissertation, Université Paris Sud-Paris XI, 2010.
10. H. Bennoui, “Interacting behavioral petri nets analysis for distributed causal model-
based diagnosis,” Autonomous agents and multi-agent systems, vol. 28, no. 2, pp.
155–181, 2014.