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