=Paper=
{{Paper
|id=Vol-1507/dx15paper14
|storemode=property
|title=Self-Healing as a Combination of Consistency Checks and Conformant Planning Problems
|pdfUrl=https://ceur-ws.org/Vol-1507/dx15paper14.pdf
|volume=Vol-1507
|dblpUrl=https://dblp.org/rec/conf/safeprocess/Grastien15
}}
==Self-Healing as a Combination of Consistency Checks and Conformant Planning Problems==
https://ceur-ws.org/Vol-1507/dx15paper14.pdf
Proceedings of the 26th International Workshop on Principles of Diagnosis
Self-Healing as a Combination of Consistency Checks
and Conformant Planning Problems
Alban Grastien
Optimisation Research Group, NICTA
Artificial Intelligence Group, The Australian National University
Canberra Research Laboratory, Australia
Abstract element of the belief state in which the plan is not ap-
plicable. To this end we define a new type of diagnoser
We introduce the problem of self healing, in that solves the following problem: find a possible be-
which a system is asked to self diagnose and haviour of the system (that agrees with the model and
self repair. The two problems of computing the observations) that ends up in a state q in which the
the diagnosis and the repair are often solved plan is not correct; this state q is added to the sample
separately. We show in this paper how to tie of the belief state so that the planner finds a more suit-
these two tasks together: a planner searches able repair plan at the next iteration. Failure on the
a prospective plan on a sample of the belief part of the diagnoser to find such a behaviour proves
state; a diagnoser verifies the applicability of that the plan is indeed correct. In practice the prob-
the plan and returns a state of the belief state lem of verifying the correctness of a plan is reduced to a
(added to the sample) in which the plan is propositional satisfiability (sat) problem that is unsat-
not applicable. This decomposition of the isfiable iff the plan is applicable in all states and that
self healing process avoids the explicit com- returns a counterexample if not.
putation of the belief state. Our experiments The contributions of this paper are i) a formal def-
demonstrate that it scales much better than inition of the self-healing problem, ii) the solving of
the traditional approach. self-healing as a combination of diagnosis and planning
steps, and iii) the reduction of each step to sat.
This work is performed in the context of discrete
1 Introduction event systems [Cassandras and Lafortune, 1999]. As
Autonomous systems are subject to faults and require opposed to supervisory control, where actions (either
regular repair actions; systems capable of performing active or passive, such as forbidding some events) are
such tasks are called self healing. Finding the optimal performed while the system is running, we follow the
repair involves solving a diagnosis problem (what may work from Cordier et al. [2007] and assume that the
the current system state be?) together with a planning repair is being performed whilst the system is inactive.
problem (what optimal/near optimal course of actions, The paper is divided as follows. Next section defines
applicable in all of the possible states, leads to an ac- the self-healing problem formally. Section 3 presents
ceptable state?). In large, partially observable, systems the proposed algorithm with a set-based perspective.
computing an explicit “belief state” can be intractable; The sat implementation is presented in Section 4. Ex-
finding a plan applicable in all elements of this belief perimental validation is given in Section 5. A compar-
state can be also intractable. ison with other problems and approaches is given in
In this paper we propose a method that avoids these Section 6.
two intractable problems. This method relies on the in-
tuition that the full belief state is not necessary to find 2 Problem Definition
the appropriate repair. For instance, if a self-healing The problem we are addressing is illustrated on Fig-
problem requires to make sure that n given machines ure 1. We are concerned with finding the most appro-
are turned off and if the status (on or off) of these ma- priate repair for a partially observed system that has
chines is unknown, then the belief state is comprised of been running freely.
2n states. However the optimal plan (press the stop but- We assume that the system can run in two different
ton on every machine) happens to be the optimal plan modes: the “active” (and useful) mode in which the
of the state where none of the machines has been shut: system is free to operate (left half of the figure) and
this single state is “representative” of all the states in the “repair” mode in which the system state is being
the belief state. re-adjusted (right half). The system behaves quite dif-
Our approach uses a planner to compute an opti- ferently in the two modes. In the active mode, the sys-
mal plan for a small sample of the belief state (at most tem is partially observable but uncontrolled. In the re-
dozens of elements); the plan is applicable in all these pair mode, the system is not observed albeit controlled;
states and leads to the goal state. In order to vali- the state changes only through explicit application of
date the plan for the full belief state we search for an actions; and special attention must be made to their
105
Proceedings of the 26th International Workshop on Principles of Diagnosis
Initial state Current state (unknown) Goal state
e1 e2 ... en−1 en a1 a2 ... ak−1 ′ ak
q0 q1 qn−1 qn=q0′ q1′ qk−1 qk′
Partially observed,
Repair plan (problem solution)
uncontrolled, behaviour
Figure 1: Schematic description of the self-healing problem: find a repair plan that returns the state in the goal
set.
applicability/effects. One reason for assuming that the Notice that a plan is a simple sequence: we do not as-
system does not run freely in the repair mode is that we sume that additional observations are available at run-
do not want to consider scenarios where faults can oc- time. There is no probing action available. After non
cur during the repair, which would increase the overall deterministic action effects, the use of conditional plans
complexity of the problem. We believe that this limi- is a second natural extension of this work.
tation, essentially the fact that the repair actions have
deterministic effects, can be lifted. Definition 2 The self-healing problem is a pair P =
hM, Oi where M is a model and O is an observation.
2.1 Explicit Model A repair plan for P is a plan that is guaranteed to be
We are considering discrete event systems (DES, [Cas- correct in the current state. Formally a repair plan is
sandras and Lafortune, 1999]). The system is modeled a plan π such that
as a finite state machine, i.e., a finite set Q of states 1 e n e
∀ρ = q0 −→ . . . −→ qn .
together with a set T of transitions labeled with finitely-
(q0 ∈ I ∧ obs(ρ) = O ∧ qn 6∈ U ) ⇒ π(qn ) ∈ G.
many events/actions.
(1)
Definition 1 An explicit self-healing system model is
a tuple M = hQ, I, Σ, Σo , Σa , T, G, U i where The set of repair plans is denoted Π(M, O) or simply
Π.
• Q is a finite set of states, I ⊆ Q is a set of initial Given a cost function on sequences of actions, the
states, G ⊆ Q is a set of goal states, U ⊆ Q is a objective of the self-healing problem is to find a cost-
set of unstable states, minimal repair plan (for simplicity we assume that such
• Σ is a finite set of events, Σo ⊆ Σ is the set of a plan exists):
observable events, Σa ⊆ Σ is the set of actions,
and π ⋆ = arg min cost(π).
π∈Π
• T ⊆ (Q × Σ × Q) is the set of transitions hq, e, q ′ i
e This definition assumes a cost function that provides
also denoted q −→ q′ . a total order on the plans. In practice we will try to
e
In the active mode the system takes a path ρ = q0 −→ 1
minimise the number of actions (all actions have the
en
. . . −→ qn such that {e1 , . . . , en } ⊆ Σ \ Σa , q0 ∈ I and same cost, the cost is cumulative) and break ties at
qn 6∈ U . This last condition is used to prevent situ- random.
ations where a fault happened right before the repair We see two main categories of self-healing problems,
is applied, i.e., before any observation of this fault was namely i) a recurring situation where the system is
made. This assumption is similar to the one made, e.g., stopped regularly, which provides a good opportunity
by Lamperti and Zanella that the system is quiescent to perform corrective actions on the system; ii) a situa-
(no more event is about to happen) when diagnosis is tion where a diagnoser/monitor detects an anomaly on
performed [Lamperti and Zanella, 2003]. This assump- the system and triggers a self-healing procedure. The
tion can be removed by assuming U = Q. Finally the present work is independent from how the problem was
observation O = obs(ρ) of this path is the projection prompted.
of e1 , . . . , en on the observable events Σo (i.e., all non-
observable events are eliminated from the sequence). 2.2 Solving the Problem Explicitly
In the repair mode a sequence of actions, called a plan This paper works under the assumption that the sys-
π = a1 , . . . , ak , is applied ({a1 , . . . , ak } ⊆ Σa ). From tem model is very large and that it is impractical to
state q0′ ∈ Q, the application of π leads to the (single) manipulate sets of states. We discuss this issue here
a1 ak
state qk′ = π(q0′ ) such that q0′ −→ . . . −→ qk′ . We assume and present some notations.
that every action is applicable in every state (if this is The simplest way to solve the self-healing problem
not the case a non-goal sink state can be created where is to compute the belief state and then compute the
all inapplicable actions lead to) and have deterministic optimal plan for this set of states.
effects. If π leads q0′ to a goal state, we say that π is Given a model M and the observation O, the belief
correct for q0′ . state B O is defined as the set of states that the system
106
Proceedings of the 26th International Workshop on Principles of Diagnosis
could be in: Finally we look at a formulation of the planning prob-
e1 en lem that is complementary to the computation of the
BO = {q ∈ Q | ∃ρ = q0 −→ . . . −→ qn . belief state. Assume that a plan π is given and we want
q0 ∈ I ∧ obs(ρ) = O ∧ qn 6∈ U ∧ q = qn }. to compute the set of states B π in which the plan π is
Notice that the definition of the belief state matches correct: B π = {q ∈ Q | π(q) ∈ G}.
the first part of Equation (1). Lemma 1 Plan π is a correct plan iff B O ⊆ B π .
def
Writing B π = Q \ B π the set of states for which π is
A conformant plan for the set of states B O is a plan
π that is correct for all states of B O : ∀q ∈ B O . π(q) ∈ G not correct, plan π is a correct plan iff B O ∩ B π = ∅.
(cf. Figure 2). Compared to the general definition of a
conformant plan (a more detailled comparison is given 3 Set Formulation of Self-Healing
in Section 6) we only deal with uncertainty on the initial We first present a formulation of our solution that is
state and we assume that actions have deterministic based on sets and that does not consider implementa-
effects. Conformant planning is provably pspace-hard tion issues (presented in the next section).
for explicit models. We propose a lazy approach to self-healing. In this
We consider the conformant planning problem from approach we search a correct plan for a sample of the
the initial set of states B O and use b = |B O | to denote belief state (a “belief sample”) and then search for a
the size of B O . The problem can be solved by consid- state of the belief state in which the plan is not applica-
ering the finite state machine M ′ where each state of ble; this state is added to the sample and the procedure
M ′ is a set of states of the original model and each is iterated again until a robust plan has been found.
transition from state S labeled by action a leads to We first give the theoretical results that justify the
S ′ = {q ′ ∈ Q | ∃q ∈ S. hq, a, q ′ i ∈ T }. The initial algorithm presented at the end of the section.
state of M ′ is B O ; a state S of M ′ is a goal state if In the following we use the notations B O and B to
it satisfies S ⊆ G. A plan π is a sequence of actions represent sets of states such that B ⊆ B O . B O will
such that π(B O ) (in M ′ ) is a goal state. Because the represent the belief state and B a small subset (a few
original model is deterministic the transition hS, a, S ′ i elements) of B O . S, S ′ will represent any set of states.
is such that the size of S ′ is smaller than S. The num- Let Π(q) be the set of repair plans that are correct
ber of statesin M ′is bounded by the sum of binomial for state q. Let Π(S) be the set of repair plans that are
|Q| |Q| correct whichever
T is the current state from S. Then
coefficients + ···+ .
1 b Π(S) = q∈S Π(q). Notice that Π = Π(B O ).
A trivial result is:
Initial states B Goal states S ⊆ S ′ ⇒ Π(S) ⊇ Π(S ′ ).
A consequence of this proposition is that the optimal
q01 q11 ... 1
qk−1 qk1 repair for B O is a correct plan for B. Computing the
optimal repair plan for the latter may therefore yield
.. .. .. .. .. the optimal plan for the former. Let π ∗ (S) be the op-
. . . . . timal plan for a set of states. The next proposition
determines how to characterize that an optimal plan
q0b q1b ... b
qk−1 qkb was found:
S ⊆ S ′ ∧ (π ∗ (S) ∈ Π(S ′ )) ⇒ π ∗ (S) = π ∗ (S ′ ).
Figure 2: Solving conformant problems; the vertical This result can be derived from the previous propo-
lines mean that the transitions are labeled by the same sition. π ∗ (S ′ ) belongs to Π(S) since S ⊆ S ′ ; therefore
action. π ∗ (S) is better than (or equal to) π ∗ (S ′ ). However, if
π ∗ (S) ∈ Π(S ′ ) and yet π ∗ (S ′ ) 6= π ∗ (S), then π ∗ (S ′ )
The model M ′ presented before cannot be easily ex- must be strictly better than π ∗ (S), which contradicts
pressed in planning modeling languages such as strips what was just said.
or pddl, or implemented in sat. Another reduction, to Applied to S = B and S ′ = B O ⊇ B, this means
M ′′ , can be introduced whose states are tuples (with b that π ∗ (B) ∈ Π(B O ) implies π ∗ (B) = π ∗ (B O ).
elements) of states from the original model: Q′′ = Qb .
A tuple state is a goal state if all its elements are in the We reuse the notation B π for the set of states in
goal: G′′ = Gb . The transitions in M ′′ correspond to which the plan π is correct, and B π = Q \ B π for the
the parallel execution of the same action in each state set of states in which it is not. With this notation,
of the tuple (represented by the vertical lines on Fig-
π ∗ (B) ∈ Π(B O ) is equivalent to B O ∩ B π∗ (B) = ∅.
ure 2).
Assume that there exists a procedure
In general M ′′ is larger than M ′ . The model also con-
verify applicability (S, π) that extracts a state
tains symmetries that efficient implementations might
need to address explicitely: for instance in model M ′′ q ∈ S ∩ B π if such a state exists, and returns ⊥
states hq1 , q2 i and hq2 , q1 i are different while they would otherwise. Then, for S ⊆ S ′ , the following results are
be the same in M ′ : {q1 , q2 } = {q2 , q1 }. trivial:
Clearly this type of approach is only applicable if B O • verify applicability (S ′ , π ∗ (S)) = ⊥ ⇒ π ∗ (S) =
comprises no more than a few dozen elements. π ∗ (S ′ );
107
Proceedings of the 26th International Workshop on Principles of Diagnosis
• let q = verify applicability (S ′ , π ∗ (S)) 6= ⊥ be a
o1
state where π ∗ (S) is not applicable, then q 6∈ S
and π ∗ (S ∪ {q}) 6= π ∗ (S) (and cost (π ∗ (S ∪ {q})) >
cost (π ∗ (S)))1 . u a2
B D G I
The first proposition shows that verify applicability can
be used to check whether the plan π ∗ (B) is correct for
B O . The second proposition indicates how a better o2 o1 a1 a1
prospective plan can be computed if π ∗ (B) is not cor- o1 u
rect: the addition of q to S guarantees that a different o1 o2
plan will be generated. A C E F H
These results lead to the procedure presented in Al- o2 a2
a2
gorithm 1. In this procedure, find plan(B) is a method
that computes a conformant plan from B as defined
at the end of the previous section (and described next Figure 3: System example with two initial states (A
section). The procedure computes the optimal plan for and B), two goal states (A and G), one unstable state
a belief sample B. If verify applicability finds a state (B), two observable events (o1 and o2 ), and two actions
q ∈ B O in which this plan is not correct, then this state (a1 and a2 ; an action affects the system state only if
is added to the belief sample and a new optimal plan there is a transition).
is generated and tested.
Algorithm 1 Diagnosis algorithm for the self-healing that neither A nor D from B O were explicitly generated
problem without enumerating the belief state B O during the procedure.
B := ∅
loop 4 SAT Formulation of Self-Healing
π := find plan (B) In this section we show how Algorithm 1 can be im-
q := verify applicability (B O , π) plemented using sat. This implementation assumes
if q = ⊥ then a symbolic representation of the model, i.e., a repre-
return π sentation where states and transitions are not enumer-
else ated but are, instead, implicitly defined by a set V of
B := B ∪ {q} Boolean state variables (aka fluents) as can be found,
end if e.g., in a strips model.
end loop
4.1 Computing a Conformant Plan for B
Because i) each loop iteration adds an element to B The procedure we use to compute the optimal plan for
and ii) B O is finite, this procedure is guaranteed to ter- a belief sample relies on a sat solver and follows the
minate. The number of iteration is, in the worst case, schematic representation of Figure 2. In planning by
the size of B O ; we expect however that a handful of sat [Kautz and Selman, 1996], given a horizon k and a
calls to find plan (·) will be sufficient to find the opti- planning problem a propositional formula Φ is defined
mal plan. that is satisfiable iff there exists a sequence of actions
of length k that solves the planning problem.2 Fur-
Example thermore Φ is defined over k + 1 copies of the state
We illustrate Algorithm 1 with the example of Figure 3. variables (the state sat variables p0 to pk where p is a
Assume that the observations are O = [o1 , o2 ]. Accord- state variable) and k copies of the actions (the action
ing to the model, the belief state is B O = {A, D, F, H} sat variables a0 to ak−1 where a is an action). Φ is
(state B is unstable, so the system cannot be in this defined such that a solution to the planning problem
state). The state needs to be returned to a subset of can be trivially extracted from the satisfying assign-
{A, G}. ment (for instance, if ai evaluates to true, then the ith
Since the belief sample B0 is initially empty, Algo- action of the plan is a). If, for instance, action a sets
rithm 1 first generates the empty plan π0 = ε. The state variable p to false, Φ will be defined such that for
procedure verify applicability exhibits state F such that all i ∈ {1, . . . , k}
u o1 o2
B − → D −→ E −→ F could explain O and such that
Φ ≡ (ai−1 → ¬pi ) ∧ · · ·
plan π0 does not lead to a goal state when applied from
F . The optimal plan for B1 = {F } is π1 = a1 . This We refer the reader to the literature on planning by sat
time verify applicability extracts state H which also be- for more details on this reduction.
longs to the belief state and for which the application Given a sample B of b states we create b copies of the
of a1 leads to sink state I. The belief sample B2 now state sat variables: p1i , . . . , pbi ; the variables pℓi model
equals {F, H} and the optimal conformant plan for B2 the effects of applying the plan on the state qℓ ∈ B.
is π2 = a2 , a1 (remember that unobservable transition We stick to a single set of action sat variables and
u
F −→ H cannot trigger after the execution of a2 ). This each copy of the state sat variables is linked to this
plan is correct for all elements in the belief state. Notice
2
The value of k is initialized to 0 and incremented until
1
Remember that no two plans have the same cost. Φ becomes satisfiable.
108
Proceedings of the 26th International Workshop on Principles of Diagnosis
set. The formula Φ presented in the example above plan is finally computed the conformant planning re-
will therefore now translate as duction to sat is satisfiable while the reduction of the
applicability function is not.
Φ ≡ ai−1 → ¬p1i ∧ · · · ∧ ai−1 → ¬pbi ∧ · · ·
4.2 Verifying Correctness of a Plan 5 Experiments
Like the plan generation, plan correctness is imple- We ran some experimental evaluation of the approach
mented in sat. This time it matches the representation presented in this paper.
of Figure 1. Since the problem presented here is new, we had to
A plan is proved incorrect if an explanation of the build new benchmarks. We propose a variant of the
observations can be found in which the application of benchmark presented by Grastien et al. [2007] which
the plan leads to a non final goal (remember that all will be made available to the community. The sys-
plans are applicable). tem comprises 20 components interconnected in a torus
Once again a propositional formula is defined that is shape. Each component contains eight states, including
satisfiable iff such an explanation exists. This formula two unstable states and one goal state. The behaviour
contains two parts: sat variables pi∈{0,...,n} represent on each component can affect its neighbour and the
the state of the system in the active mode while vari- local observations cannot allow to determine anything
ables p′i∈{0,...,k} represent the state in the repair mode.3 about the local behaviour: the full system needs to
The formula is the conjunction of the formulas: be monitored in order to understand the state system.
• Φactive a propositional formula that is satisfiable Repair actions can also be local or affect several com-
iff there exists an explanation to the observa- ponents.
tions (whose final state is represented by the vari- We built 100 problem instances on this system. We
ables pn ); this type of reduction is quite standard restricted ourselves to totally ordered observations, but
[Grastien and Anbulagan, 2013]; notice that one of the benefits of using diagnostic tech-
niques is to be able to handle partially-ordered obser-
• Φ′repair a propositional formula that is satisfiable vations (observations where the order of the observed
iff there exists a state in which the proposed plan events is only partially known because the delay be-
is not correct (this state is represented by the vari- tween their reception is small compared to the trans-
ables p′0 ); mission/processing delay).
V
• p∈V (pn ↔ p′0 ), where p ranges over the state We compare our approach to a symbolic approach
variables, the formula that links the final state of that uses BDDs (specifically the buddy package) to
the active phase and the initial state of the repair track the belief state and then uses A* to find the op-
phase. timal repair plan. The heuristic used by A* is imple-
Intuitively, the assignments of the variables pn that mented as follows: a state of the system is extracted
are consistent with Φactive are a symbolic representa- from the BDD and the optimal repair is computed for
tion of B O . Formally let V be the set of variables that this state using sat; the length of this optimal repair is
appear in Φactive ; then ∃(V \ {pn | p ∈ V }). Φactive is used as a lower bound for the optimal repair from the
logically equivalent to the symbolic representation of current search node.
B O . Similarly the variables p′0 of Φ′repair represent B π . Our belief sample method uses glucose_static 4.0
[Audemard and Simon, 2009]. glucose is heavily based
As a consequence any other representation of B O or on the minisat solver [Eén and Sörensson, 2003].
B π could be used if such representations are more con- The experiments were run on 4-core 2.5GHz cpu with
venient (e.g., if they are more compact or if they help 4GB RAM, with GNU/Lunix Mint 16 “petra”. A ten
the sat solver). minutes (600s) timeout was provided.
Difference Between the Two Reductions 1000
The first reduction aims at finding a plan of length k
that is applicable in b states. Therefore it includes b × k 100
copies of the state variables and k copies of the action
Time (s)
variables. 10
The second reduction aims at finding a plan com- BuDDy
Belief Sample
posed of two parts: a trajectory in the active space and 1
0 10 20 30 40 50 60 70 80 90 100
a trajectory in the repair space. Therefore it includes Problems
n + k copies of the state variables and n copies of the
events (there could be k copies of the actions but the Figure 4: Runtime in seconds required to solve self-
value of these variables is known in advance since the healing problem instances; sorted.
plan is an input of this reduction).
An interesting difference between the two reductions
The results are summarized in Figure 4. The in-
is that the trajectories of the former should lead to goal
stances are sorted in increasing runtime, meaning that
states while the trajectory of the latter should lead to
the instance at position x for one implementation may
a non goal state. As a consequence when the repair
be different from the instance at the same position for
3
It is assumed that the length of the explanation can be the other. The approach based on the generation of the
bounded by a known value n; k is the length of the plan belief state only saw 64 instances solved before timeout,
being tested. against 83 for our approach. In general our approach
109
Proceedings of the 26th International Workshop on Principles of Diagnosis
is two orders of magnitude faster than A*, although generated [Micalizio, 2014].
we would need more benchmarks and comparisons to
understand better the strength of this approach. 7 Conclusion and Extensions
Out of the 87 instances instances solved by the Belief In this paper we presented a method to solve the self-
Sample method, 82 could be solved by exhibiting only healing problem. The problem consists in finding a
one element of the belief state. Another three instances repair plan that can lead back to a goal state a sys-
could be solved with a sample of two elements, and tem whose execution has been partially observed. We
two required a sample of three elements to generate a avoid computing the belief state. Instead we propose a
conformant plan. method whereby plans are computed on a sample of the
belief state whilst a diagnoser verifies their correctness
6 Discussion and generates an element of the belief state (added to
the sample) if the plan is not correct. Both the plan-
The objective of connecting the diagnostic and plan-
ning and the diagnosis problems are reduced to sat
ning tasks is quite ambitious. From the diagnostic per-
problems. We show that non trivial problems can be
spective, and since the seminal work from Sampath et
easily solved by this approach.
al. [1995] the problem has generally been the detection
of specific events or patterns of events [Jéron et al.,
2006]. The main inspiration of the present work is the There are many possible extensions to this work.
self-heability question asked by Cordier et al. [2007]; One issue is that enforcing a conformant plan may be
the aforementioned work is one of the first attempt to too restrictive. We want to avoid prohibitive repairs
frame diagnosis as the problem of finding the optimal in situations where the system is healthy. This is a
repair plan, although the complexity of computing the common problem in diagnosis of dynamic systems: the
plan is not addressed. In static contexts similar ques- state of the system can never be precisely determined
tions have been asked where the problem was framed as at the current time; it is often not unconceivable that
finding the optimal balance between increasing the cost a fault just happened on the system and has not had
of gathering information (observations) and improving time to develop into a visible faulty trace. The issue
the precision of diagnosis (and, consequently, reducing here is that conformant plans must provide for such
the cost of planning) [Torta et al., 2008]. contingencies even when there is no evidence for them.
Supervisory control [Ramadge and Wonham, 1989] is An implicit assumption of our work is that unhealthy
a problem very similar to self-healing. The goal is to system behaviours can be detected to a large extend.
control some actions (forbid their occurrence) in order The set of unstable states serves this purpose: they are
to meet some specification. The main difference with useful to model the fact that any “failure” in the sys-
our work is the fact that control applies continuously tem will lead to abnormal observations before a repair
while we assume that self-healing is performed when the action is performed.
system is not active (either because the repair process We see two avenues to handle situations where the
is expensive—it might require to stop the system for unstability feature cannot address the problem pre-
instance—or because it can only be performed at some sented before. First probabilities can be incorporated
time—every night for instance). Furthermore control into the model, which allows for chance-constrained
tries to be as unobtrusive as possible: it merely forbids planning [Santana and Williams, 2014]. Issues with this
some transitions and generally does not choose actions approach include the problem of building large models
to perform. with meaningful probabilities and the problem of ex-
Conformant planning [Smith and Weld, 1998] is the tending the sat reduction to deal with probabilities
problem of finding a sequence of actions that is guar- (as well as scaling up to large models). A second, qual-
anteed to lead to the specified goal, despite uncertainty itative, possibility is to ignore contingencies that are
on the initial state and nondeterministic action effects. supported by no strong evidence. For instance failures
Solutions to conformant planning have been proposed that are not part of a minimal diagnosis might be ig-
that compute the belief state and run heuristic search nored.
[Bonet and Geffner, 2000] or that represent the belief Another restriction of the current approach is that
state symbolically [Cimatti and Roveri, 2000]. More the goal G is assumed to be known explicitly. Speci-
similar to our work Hoffmann and Brafman [2006] pro- fication of goal states may however be more complex:
posed Conformant-FF in which the belief state is rep- Ciré and Botea [2008] have proposed to define goals
resented implicitly by the set of initial states and the as properties of states defined in linear temporal logic
sequence of actions leading to the current state; at ev- (LTL). Other relevant goal properties is diagnosability
ery time step, a sat solver is used to determine the state [Sampath et al., 1995], i.e, the property that the obser-
variable values that can be inferred with certainty. This vations on the system will allow to detect/identify the
approach is similar to ours in the way it avoids comput- important system failures. A related issue is the incre-
ing belief states. More generally, we would like to adapt mental aspect: how to handle a repair after an active
our method to solve conformant planning problems. period following a first repair. A simple solution is to
The combination of planning and diagnosis has also assume that the initial state after the repair is the goal
been studied in the context of plan repair. There, a state.
(possibly conformant) plan is computed that assumes
that contigencies are unlikely to happen. The plan ex- Acknowledgments
ecution is then monitored and if the outcome of exe- NICTA is funded by the Australian Government
cution does not match the predictions, a new plan is through the Department of Communications and the
110
Proceedings of the 26th International Workshop on Principles of Diagnosis
event/action neighbour event/action
nf f nf
t z
N2 F2 R2 Table 1: Synchronised events
reb nf reb reb nf N (no fault); it moves to F when a fault occurs and R
when it recovers. The second part of the state is gener-
N1 back F1 back R1 back ally 0 (the component is running) and moves to 1 when
it needs to reboot and to 2 when it is rebooting. A fault
f on a component forces its neighbours to reboot. One
nf nf difficulty of diagnosis for this type of system is that the
f
observations (reb and back) do not point precisely to
N0 R0 the faulty component.
The repair consists in returning to state N0 . Most
states require action t to return to state N0 but this
action can move the neighbours of the component to
Figure 5: Active model for one component (observable state N2 . Therefore finding the optimal repair requires
events are reb and back). to order the actions carefully.
N2 F2 R2 References
[Audemard and Simon, 2009] G. Audemard and L. Si-
mon. Predicting learnt clauses quality in modern
SAT solver. In 21st International Joint Conference
on Artificial Intelligence (IJCAI-09), 2009.
z N1 s F1 R1
t [Bonet and Geffner, 2000] B. Bonet and H. Geffner.
t Planning with incomplete information as heuristic
t search in belief space. In Fifth International Con-
t ference on AI Planning and Scheduling (AIPS-00),
pages 52–61, 2000.
N0 t R0
[Cassandras and Lafortune, 1999] C. Cassandras and
S. Lafortune. Introduction to discrete event systems.
Kluwer Academic Publishers, 1999.
Figure 6: Repair model for one component (no transi-
tion means that the state is not affected by action). [Cimatti and Roveri, 2000] A. Cimatti and M. Roveri.
Conformant planning via symbolic model checking.
Journal of Artificial Intelligence Research (JAIR),
Australian Research Council through the ICT Centre 13:305–338, 2000.
of Excellence Program.
[Ciré and Botea, 2008] A. Ciré and A. Botea. Learn-
ing in planning with temporally extended goals and
A Problem Benchmark uncontrollable events. In Eighteenth European Con-
We now present the system we used in the experi- ference on Artificial Intelligence (ECAI-08), pages
ments.4 578–582, 2008.
The system includes 20 components ci,j where i [Cordier et al., 2007] M.-O. Cordier, Y. Pencolé,
ranges between 0 and 3 and j between 0 and 4. The L. Travé-Massuyès, and T. Vidal. Self-healability
component ci,j is connected to ci′ ,j ′ iff the total differ- = diagnosability + repairability. In Eighteenth
ent |i − i′ | + |j − j ′ | is at most one (where i and j are International Workshop on Principles of Diagnosis
taken modulo 3 and 4). For instance, c0,1 is connected (DX-07), pages 251–258, 2007.
to four components c0,0 , c0,2 , c3,1 , and c1,1 .
The model of one component for the active mode is [Eén and Sörensson, 2003] N. Eén and N. Sörensson.
given in Figure 5 and the model for the repair mode An extensible SAT-solver. In Sixth Conference
is given in Figure 6. The connections between com- on Theory and Applications of Satisfiability Testing
ponents implies forced transitions when some events (SAT-03), pages 333–336, 2003.
occur; these are summarised in Table 1 For instance, [Grastien and Anbulagan, 2013] A. Grastien and
when event f occurs on component c0,1 , event nf oc- A. Anbulagan. Diagnosis of discrete event systems
curs on every one of its four neighbours. using satisfiability algorithms: a theoretical and
A component state contains two types of informa- empirical study. IEEE Transactions on Automatic
tion: whether a failure occurred on the component and Control (TAC), 58(12):3070–3083, 2013.
whether it is run. The first part of the state is initially
[Grastien et al., 2007] A. Grastien, A. Anbulagan,
4
The benchmark is available at this address: J. Rintanen, and E. Kelareva. Diagnosis of discrete-
http://www.grastien.net/ban/data/bench-dx15.tar.gz. event systems using satisfiability algorithms. In
111
Proceedings of the 26th International Workshop on Principles of Diagnosis
22nd Conference on Artificial Intelligence (AAAI-
07), pages 305–310, 2007.
[Hoffmann and Brafman, 2006] J. Hoffmann and
R. Brafman. Conformant planning via heuristic for-
ward search: a new approach. Artificial Intelligence
(AIJ), 170:507–541, 2006.
[Jéron et al., 2006] T. Jéron, H. Marchand, S. Pinchi-
nat, and M.-O. Cordier. Supervision patterns in
discrete-event systems diagnosis. In Seventeenth
International Workshop on Principles of Diagnosis
(DX-06), pages 117–124, 2006.
[Kautz and Selman, 1996] H. Kautz and B. Selman.
Pushing the envelope : planning, propositional logic,
and stochastic search. In Thirteenth Conference on
Artificial Intelligence (AAAI-96), pages 1194–1201,
1996.
[Lamperti and Zanella, 2003] G. Lamperti and
M. Zanella. Diagnosis of active systems. Kluwer
Academic Publishers, 2003.
[Micalizio, 2014] R. Micalizio. Plan repair driven by
model-based agent diagnosis. Intelligenza Artificiale,
8(1):71–85, 2014.
[Ramadge and Wonham, 1989] P. Ramadge and
W. Wonham. The control of discrete event systems.
Proceedings of the IEEE: special issue on Dynamics
of Discrete Event Systems, 77(1):81–98, 1989.
[Sampath et al., 1995] M. Sampath, R. Sengupta,
S. Lafortune, K. Sinnamohideen, and D. Teneket-
zis. Diagnosability of discrete-event systems.
IEEE Transactions on Automatic Control (TAC),
40(9):1555–1575, 1995.
[Santana and Williams, 2014] P. Santana and
B. Williams. Chance-constrained consistency
for probabilistic temporal plan networks. In 24th
International Conference on Automated Planning
and Scheduling (ICAPS-14), 2014.
[Smith and Weld, 1998] D. Smith and D. Weld. Con-
formant graphplan. In Fifteenth Conference on Ar-
tificial Intelligence (AAAI-98), pages 889–896, 1998.
[Torta et al., 2008] G. Torta, D. Theseider Dupré, and
L. Anselma. Hypothesis discrimination with abstrac-
tions based on observation and action costs. In Nine-
teenth International Workshop on Principles of Di-
agnosis (DX-08), pages 189–196, 2008.
112