Diagnosability Testing with Satisfiability Algorithms

1 Introduction

Faults in dynamic systems can be diagnosed by observing a sequence of events taking place in the system and inferring the occurrence of unobservable failure events [Sampath et al., 1995]. A main question arising in this setting is whether it is always possible to infer that a failure has occurred. A system that has this property is diagnosable. The diagnosability question for transition systems with a graph representation can be solved in polynomial time [Jiang et al., 2001].

Many systems exhibit regularities best captured by representing them in terms of state variables, which also makes it possible to represent systems with very large state spaces succinctly without representing each state explicitly. The number of states of a succinctly represented system may be exponential in the size of its representation, which makes the diagnosability problem PSPACE-complete [Rintanen, 2007]. The diagnosability problem is similar to other PSPACEcomplete problems like AI planning and LTL model-checking in that it reduces to finding paths in a graph. An efficient approach to solving AI planning and model-checking problems is to reduce them to the satisfiability problem of the classical propositional logic [Kautz and Selman, 1996; Biere et al., 1999]. This suggests a similar approach to diagnosability testing, which is what we pursue in this work.

The structure of the paper is as follows. In Section 2 we present the transition system framework and formally define when a system is diagnosable. Section 3 contains the main contribution of the work, an encoding of the diagnosability problem as a formula in the classical propositional logic. In Section 4 we show how these formulae can be used to demonstrate that a system indeed is diagnosable, as opposed to showing that it is not. Section 5 contains a demonstration of the scalability of the approach to transition systems with very large state spaces, and Sections 6 and 7 conclude the paper by discussing related work and pointing out future research directions.

2 Preliminaries

We define transition systems following Sampath et al. [1995].

Definition 2.1 (Transition systems) A transition system is a tuple T = 〈X, Σo, Σu, Σf , δ, s0〉 where

• X is a set of states,
• Σo is a set of observable events,
• Σu is a set of unobservable events,
• Σf is a set of failure events,
• δ ⊆ X × (Σo ∪Σu ∪Σf ) ×X is the transition relation,
• s0 ∈ X is an initial state.

The transition system is initially in the state s0, and an event sequence e0, . . . , en-1 takes the system through a sequence s0, s1, . . . , sn of states such that (si, ei, si+1) ∈ δ for all i ∈ {0, . . . , n-1}. Note that a state si and an event ei do not necessarily determine the successor state si+1 uniquely.

Let T = 〈X, Σo, Σu, Σf , δ, s0〉 be a transition system. We say that e0, . . . , en-1 is a sequence of events in T if there are states s1, . . . , sn such that (si, ei, si+1) ∈ δ for all i ∈ {0, . . . , n - 1}.

The state sequence nor the unobservable or the failure events can be observed. In deciding whether a failure has occurred only the sequence of observable events is available.

Let σ ∈ (Σo ∪ Σu ∪ Σf)∗ be a sequence of events. We define its projection π(σ) to observable events recursively as follows.

Sampath et al. [1995] give a definition of diagnosability which we adapt to our notation.

Definition 2.2 (Diagnosability) A transition system T = 〈X, Σo, Σu, Σf , δ, s0〉 is diagnosable if there is d such that for any sequence σ of events in T that ends in a failure event and for all sequences σ1 = σσ′ and σ2 in T such that |π(σ′ )| ≥ d and π(σ1) = π(σ2), σ2 includes a failure event.

Hence a system is diagnosable if and only if there are no two infinite event sequences which have the same observable events and one of them contains a failure event and the other one not. In other words, every infinite continuation of an event sequence with a failure is distinguishable from every infinite event sequence without a failure.

The constant d is called the delay. Not all failures can be detected immediately after they have taken place, and the delay expresses how many further events have to be observed before being certain that a failure has taken place.

2.1 Succinct SystemRepresentation

The structure of many systems is highly regular and it may be more practical to represent states in terms of state variables and the relations corresponding to events in terms of changes to the values of the state variables. This often makes it possible to represent very large systems compactly.

The set of states of a system consists of all the valuations of the state variables in a finite set A. In this paper we restrict to two-valued (Boolean) state variables. Hence a state s : A → {0, 1} is a total function from the state variables to the constants 1 (true) and 0 (false). A literal is a state variable or its negation, and the set of all literals is L = A∪{¬a|a ∈ A}. The language L over A consists of all formulae that can be formed from A and the connectives ∨ and ¬. We use the standard definitions of further connectives φ ∧ ψ ≡ ¬(¬φ ∨ ¬ψ), φ→ψ ≡ ¬φ ∨ ψ and φ ↔ ψ ≡ (φ→ψ) ∧ (ψ→φ).

The main design decision for succinct transition systems is how to represent transition relations. It would be possible to use arbitrary propositional formulae which is a powerful and general representation, but as our intention is to utilize independence of events for obtaining more efficient diagnosability testing, we have decided to use a more restricted representation that makes it possible to define what does it mean that two or more events take place simultaneously.

Definition 2.3 (Succinct transition systems) A succinct transition system is a tuple 〈A, Σo, Σu, Σf , δ, s0〉 where

• A is a finite set of state variables,
• Σo is a set of observable events,
• Σu is a set of unobservable events,
• Σf is a set of failure events,
• δ : Σo ∪Σu ∪Σf → 2L×2L assigns each event a set of pairs 〈φ, c〉, and
• s0 is an initial state (a valuation of A).

An event e ∈ Σo ∪ Σu ∪ Σf is described by a set of pairs 〈φ, c〉 which indicate that the event can be associated with changes c in states that satisfy the condition φ. More formally, an event e ∈ Σo ∪ Σu ∪ Σf is possible in any state s such that s |= φ for some 〈φ, c〉 ∈ δ(e). When e takes place in s, one of the pairs 〈φ, c〉 ∈ δ(e) satisfying s |= φ is chosen and the effect of the event is that the literals in c become true.

Let s be a state and c a consistent set of literals. Then define the successor state s′ = succ(s, c) of s with respect to c by

1. s′ (a) = 1 for all a ∈ A such that a ∈ c,
2. s′ (a) = 0 for all a ∈ A such that ¬a ∈ c, and
3. s′ (a) = s(a) for all a ∈ A that do not occur in c.

A succinct transition system can be mapped to a transition system as follows.

Definition 2.4 Let T = 〈A, Σo, Σu, Σf , δ, s0〉 be a succinct transition system. Then define the transition system T ′ = R(T ) by R(T ) = 〈X, Σo, Σu, Σf , δ′ , s0〉 where

1. X is the set of all valuations of A and
2. δ′ = {(s, e, succ(s, c)) ∈ X × (Σo ∪ Σu ∪ Σf ) × X| 〈φ, c〉 ∈ δ(e), s |= φ}.

2.2 Simultaneous Events

An important factor of efficient SAT-based planning [Kautz and Selman, 1996] is the notion of parallel or partially ordered plans. This means that several independent actions can be taken simultaneously, and it has the advantage that it is unnecessary to consider all n! total orderings of n independent events as their mutual ordering does not matter.

Dependence is defined through the notion of interference. The pairs 〈φ1, c1〉 and 〈φ2, c2〉 interfere if there is a ∈ A that occurs positively/negatively in c1 and negatively/positively in φ2 or in c2, or positively/negatively in c2 and negatively/positively in φ1.

Events e1, . . . , en can take place simultaneously with o1 ∈ δ(e1), . . . , on ∈ δ(en) if o and o′ do not interfere for any {o, o′} ⊆ {o1, . . . , on} such that o ̸= o′ .

We will consider diagnosability testing with sequences E1, . . . ,En of (possibly empty) sets Ei of event occurrences such that all members of Ei are mutually noninterfering. We define the successor state s′ of s with respect to a set E of non-interfering event occurrences by s′ = succ(s, ⋃〈φ,c〉∈E c).

Let σ ∈ (2Σo∪Σu∪Σf )∗ be a sequence of sets of events. Its projection π(σ) to observable events is defined as follows.

For a succinct transition system we say that E0, . . . , En-1 is a sequence of parallel events in T if there are states s0, . . . , sn such that for all i ∈ {0, . . . , n - 1} si+1 = succ(si,E) for some E = {o1, . . . , ok} such that there are o1 ∈ δ(e1), . . . , ok ∈ δ(ek) where Ei = {e1, . . . , ek} and oh and oj do not interfere for any h ∈ {1, . . . , k} and j ∈ {1, . . . , k}\{h}.

Diagnosability of succinct transition systems with simultaneous events is defined analogously to Definition 2.2. The length |(E1, . . . ,En)| of sequences of sets of parallel events is defined as the sum ∑ni=1 |Ei| of the cardinalities of the sets. A small technical difference is caused by the fact that projection π(E1, . . . ,En) for sequences of parallel events always results in a sequence of the same length n (often with empty event sets.) It can be shown that the definitions are equivalent by interpreting a set of parallel events as any total ordering of the events.

3 Diagnosability as a Satisfiability Problem

Jiang et al. [2001] have shown how the diagnosability test can be reduced to finding a path in a graph. Their test is based on making the definition of diagnosability (Definition 2.2) finite by constructing a product transition system, sometimes called the twin plant, in which states are pairs (s, ˆ s) of states of the original transition system, and events represent unobservable events in one or both of the components of these state pairs, or observable events shared by both components. If in this system there is an event sequence from (s0, s0) to some (s, ˆ s) which includes a failure event in the first component but not in the second, and there is a non-empty event sequence back to (s, ˆ s) with no failures in the second component, then a pair of infinite event sequences witnessing non-diagnosability exists. This reformulation of Definition 2.2 reduces infinite event sequences to cycles in a graph.

This diagnosability test can be formulated as a satisfiability problem in the classical propositional logic, similarly to other path finding problems in AI planning [Kautz and Selman, 1996]. We construct a formula for which the satisfiable valuations correspond to pairs [(s0, . . . , sn), (ˆ s0, . . . , ˆ sn)] of state sequences with s0 = ˆ s0 that correspond to pairs [(E0, . . . , En-1), ( ˆ E0, . . . , ˆ En-1)] of event sequences such that π(E0, . . . , En-1) = π( ˆ E0, . . . , ˆEn-1) and of which one contains a failure event and the other does not, and which loop back to (si, ˆ si), that is, sn = si and ˆ sn = ˆ si for some i ∈ {0, . . . , n - 1}. The formula for a given event sequence length is satisfiable if and only if it is not possible to detect the occurrence of a failure event.

The encoding of state and event sequences is similar to the encoding of planning in the propositional logic [Kautz and Selman, 1996]. That the projections of both sequences to observable events coincide is guaranteed by forcing each observable event to take place in both sequences simultaneously. Essentially, each observable event is a joint event of both sequences.

Next we define the formula for diagnosability testing of a succinct transition system T = 〈A,Σo,Σu,Σf , δ, s0〉. The events at each time point t are described by a formula T (t, t + 1) parameterized with t. The propositional variables occurring in the formula, with superscripts t referring to different times points, are the following.

• at and ˆat for all a ∈ A and t ∈ {0, . . . , n}.
• eto for all e ∈ Σo ∪ Σu ∪ Σf and o ∈ δ(e) and t ∈ {0, . . . , n - 1}.
• ˆ eto for all e ∈ Σo ∪Σu, o ∈ δ(e) and t ∈ {0, . . . , n-1}.
• et for all e ∈ Σo and t ∈ {0, . . . , n - 1}.

Propositional variables with a hat ˆa represent event occurrences and values of state variables in the second event sequence that does not contain failure events. The propositional variables et describe the occurrence of observable events simultaneously in both event sequences.

Next we describe T (t, t + 1) for a given t. When an event occurs, the event must be possible in the current state and it has some effects.

The value of a state variable changes only if there is a reason for the change.

for all a ∈ A where o1 = 〈φ1, c1〉, . . . , ok = 〈φk, ck〉 are all event occurrences with ¬a ∈ ci and e1, . . . , ek are the respective events with oi ∈ δ(ei). For the change from false to true the formulae are defined similarly by interchanging a and ¬a.

An event can occur in only one way, and two events cannot be simultaneous if they interfere.

The above formulae describe one step of an event sequence. We need to represent two event sequences, so we have a copy of all of the above formulae in which all propositional variables at and eto have been replaced by ˆat and ˆ eto respectively. The second sequence is restricted to events in Σo ∪Σu. This is the key idea in the diagnosability test which makes it possible to identify two sequences of events that have the same observable events and only the first of which contains a failure event.

The formulae that connect the two event sequences require that observable events take place in both sequences whenever they take place.

To avoid trivial cycles we require that at every time point at least one event takes place.

The conjunction of all the above formulae for a given t is denoted by T (t, t + 1). A formula for the initial state s0 is

We define a formula that finds a pair of infinite executions (in the form of a cycle) with the same observable events and a failure in one execution but not in the other.

The possible cycles represented by ΦTn are illustrated in Figure 1. The parameter n controls the number of states in the sequence, and the last state must equal one of the preceding states so that a cycle is formed.

The diagnosability question can also be formalized with a fixed starting point m for the cycle (Figure 2.)

We show that the formulae ΦTn perform the diagnosability test correctly. Proofs for ΦTm,n are analogous.

Lemma 3.1 Let T = 〈A,Σo,Σu,Σf , δ, s0〉 be a succinct transition system and n a positive integer. The formula ΦTn is satisfiable if and only if there are sequences σ = (E0, . . . , En-1) and ˆσ = ( ˆE0, . . . , ˆEn-1) of parallel events in T such that

1. (E0 ∪ · · · ∪En-1) ∩Σf ̸= ∅,
2. ( ˆ E0 ∪ · · · ∪ ˆEn-1) ∩ Σf = ∅,
3. Ei ∪ ˆEi ̸= ∅ for all i ∈ {0, . . . , n - 1},
4. π(σ) = π(ˆσ), and
5. there are executions s0, . . . , sn of σ and ˆ s0, . . . , ˆ sn of ˆσ in T such that s0 = ˆ s0 and sm = sn and ˆ sm = ˆ sn for some m ∈ {0, . . . , n - 1}.

Proof: Sketch: Proof of the equivalence from left to right is a demonstration that a valuation that satisfies ΦTn can be mapped to σ, ˆσ and executions s0, . . . , sn and ˆ s0, . . . , ˆ sn that satisfy the required properties.

Proof from right to left is by constructing a valuation of all propositional variables in ΦTn based on σ, ˆσ and the executions s0, . . . , sn and ˆ s0, . . . , ˆ sn, and then showing that each conjunct of ΦTn is satisfied by that valuation. □

Theorem 3.2 For a succinct transition system T , ΦTn is satisfiable for some n ≥ 1 if and only if T is not diagnosable.

Proof: Sketch: We show that T is not diagnosable iff for some n the right hand side of the equivalence in Lemma 3.1 holds. Assume that T is not diagnosable. Hence there are infinite sequences σ = (E0,E1,E2, . . .) and ˆσ = ( ˆ E0, ˆE1, ˆE2, . . .)

of parallel events in T such that π(σ) = π(ˆσ) and σ contains a failure event and ˆσ does not. Let s0, s1, s2, . . . and ˆ s0, ˆ s1, ˆ s2, . . . be the corresponding state sequences.

Since T has only a finite number of states, there are some m and n such that m < n and sn = sm and ˆ sn = ˆ sm and Σf ∩ Ek ̸= ∅ for some k ∈ {0, . . . , n - 1}. Now (E0, . . . , En-1) contains a failure event and ( ˆE0, . . . , ˆEn-1) does not, and the sequences satisfy the requirements in the right hand side of the equivalence in Lemma 3.1 except for condition 3, which can be satisfied by deleting those Ei and ˆEi for which Ei ∪ ˆEi = ∅.

For the implication from right to left assume that the right hand side of Lemma 3.1 holds. Now the two sequences (E0, . . . ,En-1) and ( ˆE0, . . . , ˆEn-1) yield the infinite sequences σ = E0, . . . ,En-1,Em, . . . ,En-1, . . . and ˆσ = ˆE0, . . . , ˆEn-1, ˆ Em, . . . , ˆEn-1, . . . with π(σ) = π(ˆσ) so that σ contains a failure event and ˆσ does not. Hence T is not diagnosable. □

Search for the proof of non-diagnosability with formulae ΦTn leads to a one-dimensional search problem for the value of n, and with ΦTm,n the problem is two-dimensional. The standard solution method in the one-dimensional case is to test the satisfiability of ΦT1 , then ΦT2 and so on, until a satisfiable formula is found. There are also parallelized algorithms that may find a satisfiable formula much faster than this sequential method [Rintanen et al., 2006].

4 Showing Diagnosability

For a system that is actually diagnosable, the formulae in the previous section are not very practical for showing diagnosability because there is no simple way to guarantee that the parameter n is high enough so that all reachable states with a failure event have been covered. The most obvious upper bound for n is the cardinality of the set of all states, which is often impractically high: for q state variables one would be forced to consider n = 22q . Solutions to this problem have been proposed [Sheeran et al., 2000] but they work for specific types of transition systems only or they step outside the SAT framework [McMillan, 2003].

However, in many cases it is not necessary to include a complete reachability test. It may be sufficient to use a formula ρ which gives an upper bound to the set of state pairs (s, ˆ s) in the twin plant that could be reached by event sequences σ = (E0, . . . , Ek) and ˆσ = ( ˆ E0, . . . , ˆEk) such that π(σ) = π(ˆσ) and ( ˆE0 ∪ · · · ∪ ˆEk) ∩ Σf = ∅.

It may be possible to show that for no state pair satisfying ρ there is an event sequence starting with a failure event in the first component and another event sequence without failure events starting in the second component if both sequences must have the same observable events. This can be tested by using the following formula with increasing values of n.

The formula is satisfiable iff after a failure in the first component of the twin plant (but not in the second) an event sequence of length n with the same observable events in both components can take place. Hence, if the formula is unsatisfiable, the behavior after a failure necessarily differs from the behavior without a failure, and the system is diagnosable.

The incompleteness of this test is caused by the approximate nature of ρ: if ρ represents too many unreachable states of the twin plant, then it may appear that distinguishing between behavior with and without failure is not possible. Hence the unsatisfiability of the formula is a sufficient but not a necessary condition for diagnosability.

A complete positive and negative test for diagnosability is now obtained by testing the satisfiability of ΦTn for increasing n interleaved with testing the satisfiability of ΨT,ρ n′ for increasing n′ and increasingly strong upper approximations ρ of the reachable state pairs in the twin plant.

There are alternative ways how the formulae ρ for approximating reachability in the twin plant could be derived. One approach is by polynomial time algorithms for computing sets V of 2-literal clauses that are true in all reachable states [Rintanen, 1998]. If a state in the twin plant does not satisfy ρ = ∧ V it is unreachable from the initial state. Other approaches to deriving tighter upper bounds ρ could be based on techniques for knowledge compilation [Selman and Kautz, 1996] and OBDDs [Bryant, 1992] or DNNF [Darwiche, 2001].

5 Experiments

The algorithm of Jiang et al. [2001] is impractical because it relies on the explicit enumeration of all pairs of states. For a transition system with n states, the twin plant consists of n2 states. Starting from n = 10000 the size of the twin plant is too high for practically running their algorithm.

We demonstrate the much better scalability of our approach (Section 3) by using a system that consists of m identical interconnected components. Each component has 6 states. The number of states of the whole system with C components is therefore 6C . There are some dependencies between the states of neighboring components which means that not all 6C state combinations are actually possible. The twin plant in the diagnosability test has a quadratic number 62C of states, which becomes infeasible for explicit state enumeration starting from about C = 8 components.

Each component has 22 events of which 4 are observable. We tested the diagnosability of a faulty event in one component. To obtain bigger and bigger problems we increased the number of components. The parameter n for proving non-diagnosability was 4 irrespective of C, meaning that the shortest path with a cycle has length 4.

Statistics on formulae representing the diagnosability problem are given in Table 1. The formulae for n = 3 are unsatisfiable and for n = 4 they are satisfiable. After the first two columns for C and n we give the value of the formula (whether it is satisfiable or not), the number of propositional variables and clauses in the formula, and finally the time it took a SAT solver to test satisfiability.

The experiments were run with a 1.73 GHz Pentium 4 computer and the Siege SAT solver (version 4) [Ryan, 2003]. Since Siege is a randomizing SAT solver and the runtimes vary across different runs, we ran it 10 times with each formula and computed 95 per cent confidence intervals for the mean by using a standard boot-strapping method. These are shown in the last column of Table 1 next to the runtime.

Unsurprisingly, there appears to be an exponential growth in the runtimes, but for our system non-diagnosability can be detected rather easily for systems with 160 or 200 components and an astronomic number of states. The propositional formulae are big, with one or two hundred thousand propositional variables and one or two million clauses, but efficient SAT solvers can utilize the regularity of the transition systems to find the cyclic path in the twin plant efficiently. For systems in which the components are more complicated or in which the cycles witnessing non-diagnosability are longer, the approach probably does not scale quite as far.

6 RelatedWork

Another approach to finding paths in graphs compactly represented in terms of state variables is based on ordered binary decision diagrams (OBDDs) [Bryant, 1992]. OBDDs were very popular in computer-aided verification, especially model-checking [Burch et al., 1994], until the introduction of SAT based techniques [Biere et al., 1999] following their success in AI planning [Kautz and Selman, 1996]. The main disadvantage of OBDDs is their fast growth when the number of state variables increases. Their main advantages are generality and flexibility. For instance, it is easy to detect that an OBDD represents all reachable states, which is more difficult for SAT as discussed in Section 4.

Cimatti et al. [2003] have expressed a narrow diagnosability test, with only delays d = 1, as a model-checking problem in a temporal logic, and used a general-purpose modelchecker NuSMV for testing diagnosability.

7 Conclusions

We have presented a SAT based approach to diagnosability testing, and demonstrated its scalability to systems with billions of states. Earlier works, most notably by Jiang et al. [2001], have relied on explicit enumeration of the states and are feasible only for systems with a much smaller number of states. The success of SAT for the diagnosability problems parallels its successes in areas like model-checking and AI planning, and has been made possible by the fast progress in the development of efficient algorithms for the satisfiability problemof the propositional logic.

A weakness of the SAT approach in comparison to for example OBDD based techniques is that the diagnosability test is better suited to detecting non-diagnosability than diagnosability. However, the same weakness is present in other related SAT based techniques, including AI planning and bounded model-checking, in which the presence of (short) paths in transition graphs can be often easily detected, but the absence of paths having a given property, without length restrictions, is often much more difficult to detect. We intend to further investigate approximate reachability techniques for proving diagnosability.

Acknowledgements

We thank the members of the Knowledge Representation and Reasoning group as well as Sophie Pinchinat for interesting discussions and comments.

This research was supported by National ICT Australia (NICTA) in the framework of the SuperCom project. NICTA is funded through the Australian Government's Backing Australia's Ability initiative, in part through the Australian National Research Council.