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.
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 particular, Petri nets (PNs) have been used to represent the causal model, and so to exploit their analysis techniques to implement efficiently the diagnosis reasoning 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 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 expressions 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 definitions 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 detailed 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.
In this section, we outline some basic definitions that we need in this paper.
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 evolution 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.
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, IN IT is the set of instances of initial causes in terms of which the observations 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 = 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 Ψ − :
Where is the derivation symbol.
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:
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 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 multiset m, over a non-empty set S, is a function m ∈ [S → N] represented formally by: s∈S m(s) s.
• S M 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, m 1 , m 2 ∈ S M S and ∀n ∈ N:
(defined analogously for ).
Thus, a CPN is given by:
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 = ∅.
• 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.
where N is a CPN and µ is a function defined on P such that:
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 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.
where:
• 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.) Let µ 0 be the initial marking of N such that: ∀p ∈ P : µ 0 (p) = ∅ → p ∈ Ic. Definition 6. A marked CCPN (N, µ 0 ) is said to be safe iff:
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 ∀(x 1 , x 2 ) ∈ A:
-A(t) denotes the set of the input arcs of t.
-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(x 1 , x 2 ) denotes the expression attached to an arc (x 1 , x 2 ). Definition 7. A binding of a transition t is a function b defined on V ar(t) such that:
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:
Definition 8. Let µ be a marking, a transition t is enabled at µ iff:
Definition 9. Let t be an enabled transition in a marking µ, the firing of t changes the marking µ to anothor marking µ as follows:
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 step s = {t 1 , .., t n }, the firing of s at µ reaches the new marking µ such that µ =
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 distinguish, 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 corresponding 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 inputs of t while F W _out is the output sub-matrix of t. Furthermore, each transition 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 reaching 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: ∃t i , t j ∈ T, ∃µ i , µ j ∈ R(N, µ) :
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 considered model. Such a model is characterized by c 1 , c 2 and c 3 as initial-causes of the described causal model, and m 1 and m 2 as manifestations. The left places represent the internal states. Each place has a type, attached to it, which determines the set of colours that the token on the place is allowed to have. As a sample, the tokens residing in c 1 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. t 1 is a fork transition that is used to duplicate the input place c 1 by the marking a into c 11 and c 12 by the same token color. In F W (t 1 ), the first column corresponds to the input place c 1 , while, the last two ones correspond to the output places c 11 and c 12 . t 2 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 s 1 . The transition t 3 is as the logical and while t 5 and t 8 are as the logical or. The transition t 8 can be enabled in three cases (according to the number of lines in its matrix), the two first ones represent the case when either s 3 or s 4 is marked by a color a while the last is that when both places are marked by such a color. The transition t 5 has the same interpretation as t 8 , but only, with t 8 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 t 5 the produced color is defined according to the presence of colors in s 2 and s 4 , and here, t 5 guards the consistency of the net model.
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: -N is the CCPN model.
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 solutions 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 manifestations that have to be entailed by a solution to DP , while M − is the set of couples (p , c ) 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;
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
The notion of diagnosis solution can be now captured by the following proposition. 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 ) M − ] does not hold. By Definition 16:
And so, µ 0 is not a solution, which contradicts with our first assumption.
and that µ 0 is not a solution. By Definition 16:
As a result, µ 0 is a solution, which is a contradiction.
In order to solve a diagnosis problem given by means of a CCPN, we are interested 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 submatrix F W _in becomes output, denoted b_F W _out. While, the output submatrix 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 ([v q1 ..v qm ], b_F W (t))(p) such that, p is added to specify which place is (i.e, f ([v q1 ..v qm ], 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 > M (p) and t t.
Such that t 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 {c i } 1≤i≤n from the output places of t and adds a set of others {c j } 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 µ 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:
Definition 19. Given a marked CCPN (N, µ), let t be a fork transition such that • t = {p} and t • = {p 1 , ..., p m }, t is forced backwardly at the marking µ iff:
• t is not backwardly enabled at µ.
t where t is backwardly enabled or forced at µ.
If t is forced at µ then ∀p, p ∈ t • such that µ(p) = ∅ and µ(p ) = ∅, consider µ(p) = µ(p ).
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 backwardly 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 µ where µ ∈ R(N, µ i ). The set µ ini represents the candidate solutions to the given problem, 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 (m 1 ) = c and µ OBS (m 2 ) = a (For simplicity, we use the notation of sets in which the elements are couples of places with its markings, and so: µ OBS = {(m 1 , c), (m 2 , 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 discussed 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 represent forced ones. Notice that t 1 is forced when the place c 12 becomes marked with a color a (that is present in b_F W (t 1 )). Moreover, there is a path in the backward reachability graph whose terminal node is an inconsistent marking where the place s 1 has two different markings.
The obtained solutions are µ 1 = {(c 1 , a), (c 2 , a)} and µ 2 = {(c 1 , a), (c 2 , a), (c 3 , 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.
During the last decade, several model-based approaches and frameworks have been proposed, as improved ones, to solve fault diagnosis problem. The majority of them perform such a reasoning on the basis of PNs and their different 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 approach 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 diagnosis 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 performs a structural inversion3 of the CPN model, and so, analysing the CPN model backwardly becomes a forward analysis of its inverted one.
Our proposal differs from these by focusing on a particular side, when modelling 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.
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 subsystems 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.