Diagnosers and Diagnosability of Succinct Transition Systems

1 Introduction

Faults in dynamic systems can be diagnosed by an external diagnoser that observes the system behavior and infers the occurrence of failure events [Sampath et al., 1995]. A main problem in on-line diagnosis is the construction of diagnosers which are deterministic finite automata that keep track of the possible state of the system on the basis of the observations and detect the occurrence of faults. Existing algorithms for constructing diagnosers have exponential running times and construct diagnosers of exponential size. In this work we investigate the inherent complexity of diagnosers and the complexity of constructing them, giving tight upper and lower bounds for the sizes of smallest diagnosers and the time it takes to construct diagnosers. Our results show that the asymptotic worst-case time and memory consumption of existing algorithms cannot be improved.

The work is based on the framework proposed by Sampath et al. [1995]. Since many systems exhibit regularities best captured by representing them in terms of state variables, we also consider a more compact representation with state variables. Our results show that the exponentially more compact representation leads in the worst case to a corresponding increase of complexity.

The structure of the paper is as follows. In Section 2 we define transition systems and succinct transition systems. Section 3 defines the framework of diagnosers and diagnosability of Sampath et al. [1995]. In Section 4 we present the main results which establish the complexity of diagnosability testing. In Section 5 we derive tight upper and lower bounds for the worst-case size of smallest diagnosers. Section 6 discusses related work and concludes the paper.

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 a transition relation,
• s0 ∈ X is an initial state.

Initially, s0 is the state of the system. A sequence of events e0, . . . , en-1 takes place and the system goes through some states s0, s1, . . . , sn such that (si, ei, si+1) ∈ δ for all i ∈ {0, . . . , n - 1}.

For T = 〈X,Σo,Σu,Σf , δ, s0〉, 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. Detection of failures is based on the sequence of observable events only.

A basic assumption made by Sampath et al. [1995] is that there are no infinite event sequences exclusively consisting of unobservable events.

Assumption 2.2 There is no cycle in the transition graph consisting of unobservable events only.

2.1 Succinct SystemRepresentation

The state spaces of many systems are highly regular, and the transition relations of events can be represented more compactly in terms of changes to the values of state variables. This also makes it possible to practically represent large systems. Given a set A of state variables, a state is defined as a valuation of A. We will restrict to two-valued (Boolean) state variables but in general there may be several different values. The transition relation associated with an event can be expressed as a propositional formula on A and A′ . The set A′ consists of propositional variables a′ for every a ∈ A. When an event takes place, the variables in A represent the old values of the state variables and the variables in A′ represent the corresponding new values. For example, given state variables A = {a, b}, an event that makes a true and does not change the value of b can be expressed as the formula a′ ∧ (b ↔ b′ ). An arbitrary binary relation on the valuations of A can be expressed as a propositional formula, which suggests a succinct representation of transition systems in terms of state variables and formulae.

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 → L assigns each event a propositional formula over A ∪ A′ which represents a binary relation on the set of states, and
• s0 is an initial state (a valuation of A).

There are other types of succinct representations, for example based on Petri nets [Holloway et al., 1997]. However, the Petri net representation can be translated into the logic representation quite easily (assuming finite state Petri nets with an n-safety property), but not vice versa, so the logic representation is more general.

Any 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 R(T) = 〈X, Σo, Σu, Σf , δ′ , s0〉 where

1. X is the set of all valuations of A, and
2. δ′ = {(s, e, s′) ∈ X×(Σo∪Σu∪Σf )×X|s∪{(v′ , w) ∈ A′ × {0, 1}|(v, w) ∈ s′} |= δ(e)}.

3 Diagnosability

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

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

Diagnosability is defined as the possibility to detect every occurrence of a failure event: the continuation of every event sequence that includes a failure event will at some future time point be observationally distinguishable from every event sequence that does not include a failure event.

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

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.

Whether a system is diagnosable or not is important when trying to construct a diagnoser for it. A diagnoser is a deterministic finite automaton that recognizes sequences of observable events that correspond to sequences of events that include at least one failure event. If a system is diagnosable then a diagnoser exists.

Definition 3.2 A diagnoser is 〈Q, Σo, γ, z0, Y 〉 where

• Q is a set of states (unrelated to the transition system),
• Σo is a set of observable events,
• γ : Q×Σo →Q is a partial function,
• z0 ∈ Q is the initial state of the diagnoser, and
• Y ⊆ Q is the set of accepting states.

A sequence e0, . . . , en-1 of observable events takes a diagnoser through a sequence z0, . . . , zn of states such that γ(zi, ei) = zi+1. An execution z0, . . . , zn is accepting if zn ∈ Y . To accept means to detect a failure event.

Definition 3.3 〈Q,Σo, γ, z0, Y 〉 is diagnoser for T = 〈X, Σo, Σu, Σf , δ, s0〉 (with delay d) if

1. for every sequence e0, . . . , en, en+1, . . . , em of events in T such that {e0, . . . , en-1} ⊆ Σo ∪ Σu and en ∈ Σf and |π(en+1, . . . , em)| ≤ d, there is a prefix of π(e0, . . . , en, en+1, . . . , em) which the diagnoser accepts, and if
2. for a sequence e0, . . . , em of events in T the diagnoser accepts π(e0, . . . , em) then for some n ∈ {0, . . . ,m1}, en ∈ Σf , {e0, . . . , en-1} ⊆ Σo ∪ Σu and |π(en+1, . . . , em)| ≤ d.

We can define diagnosers for succinct transition systems analogously through the reduction to transition systems.

In some cases there is no finite upper bound on how long it may take before a failure is detected. For a system to be diagnosable the delay must be bounded.

Example 3.4 (Unbounded delay) Consider the transition system in Figure 1. In the starting state two events are possible, of which the leftmost one is a failure event. After this an

b

Figure 2: Delay may be quadratic in the number of states

unbounded number of unobservable events A may take place before the failure is diagnosed upon the occurrence of the observable event B. ■

A bounded delay may be quadratic in the number of states.

Example 3.5 (Quadratic delay) There are transition systems with a quadratic delay as depicted in Figure 2 [Grastien, 2006]. Of two sequences σ and σ′ such that π(σ) = π(σ′ ) = aaaaabaaaacaaadaaea the first begins with a failure event but the second does not. The sequence σ′ can continue with a but σ cannot. This can be generalized to any number n of states. The delay is (n - 2) + (n - 3) + · · · + 3 + 2 = (n-1)(n-2) 2 -1 which is O(n2 ) in the number of states. ■

This is also an upper bound on bounded delays.

Theorem 3.6 For a transition system with n states, if the system is diagnosable, then the delay is ≤ |X|2-|X| 2 where |X| is the number of states.

Proof: Assume s0e0s1e1 · · · · · · sm-1em1 smem and ˆ s0e0 ˆ s1e1 · · · · · · ˆ sm-1em1 ˆ sm ˆ em are two equally long sequences of observable events interleaved with states that are distinguished at the last step (and not before) and of which the first contains an unobservable failure event and the second does not. All unobservable events and states other than s0 and those immediately preceding an observable event are not included in the above sequences.

For the sake of argument assume that there are pairs of states si, ˆ si and sj, ˆ sj such that j > i, si = sj and ˆ si = ˆ sj . Now the sequence ei, . . . , ej-1 of events between these pairs of states could be repeated arbitrarily many times to have a pair of much longer sequences of events that are distinguishable only after the last event. This would violate our assumption that the delay is bounded.

Hence there are no i and j such that si = sj and ˆ si = ˆ sj , which entails that every pair si, ˆ si occurs only once in the sequence. This entails that the length m of the sequences, and therefore the delay, is at most |X|2 - |X|.

This bound can be tightened to |X|2-|X| 2 by noticing that there cannot be i and j such that si = ˆ sj and ˆ si = sj, or in other words, the order of the states in the pairs does not matter. □

4 Complexity of Testing Diagnosability

Jiang et al. [2001] have shown that diagnosability testing is in P. In this section we will show that this complexity upper bound is not tight. Our results also show that the EXPTIME upper bound for the diagnosability problem of succinct transition systems implied by the result of Jiang et al. is not tight.

A system is not diagnosable if there are two infinite event sequences which have exactly the same observable events and of which one contains a failure event and the other not. If this condition is not fulfilled, then every continuation of an event sequence with a failure is distinguishable from all event sequences without a failure.

Jiang et al. [2001] showed how this test can be made finitary for finite state systems, and how it can be done in polynomial time. The basic construction is a product transition system, sometimes called the twin plant, in which states are pairs (s, ˆ s) of states of the original system, and events represent unobservable events in one or both of the components of these state pairs, or observable events shared by both components. Failure events take place only in the first component of each state pair. 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, and a non-empty event sequence back to (s, ˆ s) then a pair of infinite event sequences witnessing nondiagnosability exists.

Candidate states (s, ˆ s) are found by Tarjan's strongly connected components (SCC) algorithm [Tarjan, 1972]: every node contained in a nontrivial SCC is in a cycle contained in the SCC. After finding the SCCs the diagnosability test reduces to finding a path through a failure event from (s0, s0) to some (s, ˆ s) in a non-trivial SCC. If such a path exists the system is not diagnosable.

Constructing the twin plant can be done in quadratic time in the number of states. Finding the SCCs is linear time in the number of states in the twin plant, and finding a path to a nontrivial SCC through a failure event can be done in polynomial time. Hence the diagnosability problem is in the complexity class P. However, this complexity upper bound is not tight.

We define the language NONDIAG which consists of all non-diagnosable transition systems in some suitable representation.

Our first result shows that determining non-diagnosability can be done by using only logarithmic space by a nondeterministic Turing machine, and hence the decision problem associated with NONDIAG is in NLOGSPACE. This complexity class is included in P but it is not known whether the inclusion is proper [Johnson, 1990].

Theorem 4.1 NONDIAG is in NLOGSPACE.

Proof: The proof is similar to the NLOGSPACE membership proof of testing the existence of a path between two nodes in a graph. We give a nondeterministic algorithm that takes logarithmic space. The alorithm's only data structure that does not have a constant size is the binary counter for counting up to n2 where n is the number of states. A cycle is detected as in the P-time proof of Jiang et al. [2001]. The algorithm starts from the pair (s0, s0) of initial states and nondeterministically chooses an event and a successor state for each member of the pair. The event for the second state may not be a failure, and an observable event must always be shared by both components of a state pair. The counter counts the steps. After a number of steps, including at least one failure event, the algorithm reaches a starting state (s, ˆ s) for a cycle. After this a sequence of events leading back to (s, ˆ s) is nondeterministically chosen. The Turing machine accepts if a cycle is completed before the counter reaches n2 . The Turing machine rejects if the counter reaches n2 before completing the cycle and encountering a failure event. □

We also have a simple proof of NLOGSPACE-hardness.

Theorem 4.2 NONDIAG is NLOGSPACE-hard.

Proof: We sketch a deterministic logarithmic space reduction from the NLOGSPACE-complete problem of testing whether a node in a directed graph is reachable from another node [Johnson, 1990].

Let G = 〈V, E〉 be a directed graph for which the existence of a path from s ∈ V to t ∈ V is tested. The reduction with only logarithmic space proceeds by reading the input graph G and outputting a corresponding transition system where states are the nodes of G and edges of G correspond to an observable event. The initial state of the transition system is s. The transition system additionally has a failure event F and an unobservable event NF which may take place in the state t. Both events lead to the same (arbitrary) state in V . Now the transition system is not diagnosable if and only if t is reachable from s. Construction of the transition system takes logarithmic space (actually only constant space.) □

Similarly to NONDIAG we define the language SUCCINCT-NONDIAGwhich consists of succinct transition systems that are not diagnosable.

Theorem 4.3 SUCCINCT-NONDIAG is in PSPACE.

Proof: Sketch: We could prove NPSPACE membership similarly to Theorem 4.1 and then use the equality PSPACE=NPSPACE. Alternatively, we could give a deterministic algorithm for finding a path in a graph with polynomial recursion depth and space consumption following Bylander [1994]. □

The PSPACE upper bound can be shown to be tight.

Theorem 4.4 SUCCINCT-NONDIAG is PSPACE-hard.

Proof: We reduce the halting problem of deterministic Turing machines with a polynomial space bound to the succinct diagnosability problem, showing the latter PSPACE-hard.

Part of the reduction is like in the reductions to some other succinct graph reachability problems [Bylander, 1994]. We can represent the Turing machine configurations, including the contents of a polynomially long tape, in terms of a polynomial number of state variables, and we can represent the transitions of the Turing machine in terms of a formula δ(e) which represents an unobservable event.

We construct a transition system that is diagnosable if and only if the Turing machine accepts. First a failure event F or an unobservable non-failure event NF takes place. In the non-failure case this is followed by an infinite sequence of events 1. In the failure case a simulation of the Turing machine follows. If the Turing machine accepts then an event 2 takes place. This makes it possible to distinguish between the failure and non-failure cases. So the system is diagnosable if and only if the Turing machine accepts.

Given a Turing machine, we define the succinct transition system T = 〈A, Σo, Σu, Σf , δ, s0〉 where

• A consists of all the state variables needed for encoding executions of the Turing machine with a bound on the number of used tape cells (see for example Bylander [1994]) and the state variable f that indicates that a failure has taken place and I that indicates that the execution has not started yet.

where TM is a formula for simulating the change in the Turing machine configuration in one execution step and a is a state variable that represents the accepting internal state of the Turing machine. If the Turing machine rejects it continues with event 1 indefinitely.

When the Turing machine accepts at least one event 2 takes place.

• s0 is a valuation that encodes the initial configuration of the Turing machine and sets s0(I) = 1.

□

Hence the succinct diagnosability problem is PSPACEcomplete, like some other path-finding problems in succinctly represented graphs, the succinct s-t-reachability problem [Lozano and Balc´azar, 1990] and the plan existence problem of AI planning [Bylander, 1994]. This further suggests similar approaches to solving the diagnosability problem, for example reduction to the propositional satisfiability problem SAT [Rintanen and Grastien, 2007].

5 Size of Diagnosers

In this section we show that, assuming a sufficiently restricted definition of diagnosers, sometimes diagnosers are necessarily quite large.

The size of diagnosers strongly depends on how complex computation they are allowed to perform. The more complex the computation may be the smaller the diagnoser. There are diagnosers that are Turing machines with only a constant size and that only need memory for storing the system description and the set of all states, but executing such a diagnoser may be too expensive for real-time on-line diagnosis.

In this section we focus on diagnosers that are finite automata which can process each observation in constant time.

5.1 Upper Bounds on Size

We use the notion of belief states to derive an upper bound on the size of smallest diagnosers. The basic construct is similar to that used by Sampath et al. [1995] and the size of smallest diagnosers follows from the construct by Sampath et al.

Let T = 〈X, Σo, Σu, Σf , δ, s0〉 be a transition system. Let G0(T) = 〈V,E〉 be a graph in which the set of nodes V = 2X×2Σf is the set of all sets B ⊆ X × 2Σf of pairs (s, f) ∈ X × 2Σf , and there is a labelled edge (B, e,B′ ) ∈ E from B ∈ V to B′ ∈ V if and only if either

• e ∈ Σf and B′ = {(s′ , f ∪ {e})|(s, f) ∈ B, (s, e, s′ ) ∈ δ}, or
• e ∈ Σo ∪Σu and B′ = {(s′ , f)|(s, f) ∈ B, (s, e, s′) ∈ δ},

A belief state B with (s, f) ∈ B means that it is possible that s is the current state and its history includes exactly the failure events in f. Note that it is possible that (s, f) ∈ B and (s, f ′ ) ∈ B for some f ̸= f ′ .

The initial node of the graph is BI = {(s0, ∅)}.

The number of belief states B ⊆ X × 2Σf is 2|X|2|Σf | . This is O(2n ) where n is the number of states.

This graph compactly encodes the states that could be reached by a given event sequence and the failure events in that sequence: starting in the initial node follow the edges corresponding to the events, and if (s, f) ∈ B for the node B that is reached, then it is possible to reach s with that event sequence which includes the failure events in f .

A diagnoser cannot observe unobservable events, so we construct a second graph G(T ) that represents the diagnoser's view of the possible current states and their failure histories in terms of observable events. This construction takes polynomial time in the size of G0(T). Any path e1, . . . , en, e in G0(T ) such that e is observable and e1, . . . , en are unobservable is represented in G(T ) by one edge with the label e.

Given G0(T ) = 〈V, E〉 define G(T ) = 〈V, E′ 〉 as follows. There is an edge (B, e, B′ ) ∈ E′ if and only if

• e ∈ Σo and
• B′ = ⋃mi=1 Bi where B1, . . . ,Bm are all the nodes in G0(T) such that for all i ∈ {1, . . . ,m} there is a path e1, . . . , en, e from B to Bi such that n ≥ 0 and {e1, . . . , en} ⊆ Σu ∪ Σf .

By Assumption 2.2 n is bounded by some constant ≤ |X|. The graph G(T ) has the same nodes as G0(T ) and the number of edges is at most as high.

Lemma 5.1 Let σ be a sequence of events in a system T , starting in its initial state s0, in which exactly the failure events in f occur before the last observable event and s is the last state that is not immediately preceded by an unobservable event (it is preceded by an observable event or it is the first state s0.) Then the sequence π(σ) in G(T ) leads from {(s0, ∅)} to B such that (s, f) ∈ B.

Lemma 5.2 Let T be a system with the initial state s0. Let σ be a sequence of observable events. If σ leads in G(T) from {(s0, ∅)} to B such that there is some (s, f) ∈ B, then there is a sequence σ′ of events in T such that σ = π(σ′ ) and σ′ leads from s0 to s in T and σ′ includes exactly the failure events f .

Finally, we show that G(T) is a diagnoser. The accepting states B of this diagnoser are those that include a known past failure: ⋂(s,f)∈B f ̸= ∅.

Theorem 5.3 Let T = 〈X,Σo,Σu,Σf , δ, s0〉 be a system that is diagnosable with delay d.

1. Let σ = e1, . . . , en be a sequence of events in T starting in s0 and assume en ∈ Σf . Then for every sequence of events e′1, . . . , e′m such that |π(e′1, . . . , e′m)| = d and e1, . . . , en, e′1 , . . . , e′m is a sequence of events in T , there is m′ ≤ m such that π(e1, . . . , en, e′1 , . . . , e′m′ ) leads in G(T ) from {(s0, ∅)} to B such that en ∈ ⋂(s,f)∈B f .
2. If for a sequence of events e1, . . . , em in T the path π(e1, . . . , em) in G(T) leads from {(s0, ∅)} to B and there is e ∈ ⋂(s,f)∈B f , then e ∈ {e1, . . . , em}.

Proof: For (1) take any σ′ = e′1, . . . , e′m such that |π(σ′ )| = d and σσ′ is an event sequence in T . Let B0, . . . ,Bn+m be the belief states on the path π(σσ′ ) in G(T ).

Assume en ̸∈ ⋂(s,f)∈Bn+m f. By Lemma 5.2 there is a sequence σ2 of events such that π(σ2) = σσ′ and en does not occur in σσ′ . This contradicts the fact that the system is diagnosable with delay d: for all sequences σ1 = σσ′ and σ2 of events in T such that |π(σ′ )| ≥ d and π(σ1) = π(σ2), σ2 includes the event e. Hence it must be that en ∈ ⋂(s,f)∈Bn+m f. Now en ∈ ⋂(s,f)∈Bn+m′ f for some m′ ≤ n + m.

For (2) assume that e1, . . . , em is a sequence of events in T such that the path π(e1, . . . , em) in G(T ) leads from {(s0, ∅)} to B such that there is e ∈ ⋂(s,f)∈B f .

Let σ = π(e1, . . . , em). Let m′ be the least m′ such that em′ is an observable event, and let s be the state immediately following em′ . Let σ = π(e1, . . . , em′ ) = π(e1, . . . , em). By Lemma 5.1 (s, f) ∈ B where f = Σf ∩ {e1, . . . , em}. Since e ∈ ⋂(s,f)∈B f, e ∈ {e1, . . . , em′} ⊆ {e1, . . . , em}. □

• δ = {((B, e),B′ )|(B, e,B′ ) ∈ E′} and
• A = {B ∈ V | ⋂(s,f)∈B f ̸= ∅}.

Hence the graph G(T) = 〈V,E′ 〉 corresponds to a diagnoser for T . The diagnoser starts from the node {(s0, ∅)}. After observing an event e ∈ Σo it follows the corresponding edge in the graph. Notice that unlike in the underlying system, each event in the graph 〈V,E′ 〉 leads to a unique successor node. When reaching a node B = {(s1, f1), . . . , (sn, fn)} with f = ⋂ni=1 fi ̸= ∅, the diagnoser has detected the failure events f .

The number of nodes in 〈V,E′ 〉 is O(2n ) in the number n of states in T . Some diagnosers may have more nodes than 〈V, E′ 〉 but those diagnosers are not the smallest ones. Hence the size of the smallest diagnoser is O(2n).

Since a transition system may be exponentially bigger than its succinct representation, the O(2n) bound on the diagnoser size for enumerative representations yields a O(22n ) bound on the size of diagnosers of succinct transition systems.

5.2 Lower Bounds on Size

We derive an exponential lower bound on the worst-case size of smallest diagnosers by constructing a system for which the smallest diagnoser has an exponential number of states. The high number of states in the smallest diagnoser is an indication of the need for the diagnoser to remember the past events. The number of possible past histories may grow exponentially in the size of the system and the length of the histories. The past histories may have to be encoded in the diagnoser and this leads to an exponential size.

Theorem 5.4 There are diagnosable systems for which the smallest diagnoser has size Θ(2n) where n is the number of states.

Proof: Consider the system in Figure 3. Let Σ =

{A,B,C,D}. The events of the transition system are a and ˆa for a ∈ Σ. In the initial state an unobservable event takes place. Then a sequence of |Σ| events takes place, either a or ˆa for every a ∈ Σ, followed by either an unobservable failure or an unobservable non-failure event. A failure event has taken place iff for some a ∈ Σ both a and ̂a have taken place.

The number of different sequences of observable events before the failure events is 2|Σ| . No information on these sequences can be ignored before the last event has taken place. Hence the smallest diagnoser has 2|Σ| states for representing the first |Σ| events.

Clearly, similar systems can be constructed for arbitrary sets Σ, and the number of states of these systems grows quadratically in the cardinality of Σ and the number of states in the diagnosers grows exponentially. □

We adapt the construction in Theorem 5.4 to succinct transition systems by replacing the events A,B,C,D by sequences of events corresponding to binary numbers, and utilizing the regularity of the system to represent it more compactly so that the number of states is exponential in the size of the system description. This means that the number of nodes in the diagnoser is doubly exponential Ω(22n ) in the size of the system description.

Theorem 5.5 There are succinct systems for which the smallest diagnoser has size Θ(22n ).

Proof: Let n be a size parameter that characterizes the number 2n of things to remember just like A, B, C, D in the proof of Theorem 5.4. Instead of producing a sequence of events A, ̂ A, B, ̂ B, C, ̂ C D, ̂D indicating the different "values" of A, B, C and D, the succinct system produces a sequence v0, . . . , v2n-1 of 2n events 0 or 1 followed by an unobservable failure or non-failure event, and then an event 0 or 1 for indicating a value v and a sequence of n events 0 or 1 that encodes an index i ∈ {0, . . . , 2n -1} to the first sequence. If the value vi does not match v then a failure has taken place. The construction with n = 2 is illustrated in Figure 4.

Because of space restrictions we cannot present the system here. The number of states of the system is exponential in n, and the size of the succinct representation of the system is linear in n. The size of the smallest diagnoser is exponential in the number of states and doubly exponential in n. □

6 RelatedWork and Conclusions

We have shown that the diagnosability problem of succinct transition systems is PSPACE-complete. We also tightened an earlier known polynomial time upper bound of diagnosability testing of explicitly represented transition systems by showing that non-diagnosability is NLOGSPACE-complete.

The work by Sampath et al. [1995] underlies much of the work in the diagnoser framework, and also our belief state enumeration algorithm in Section 5.1 is based on it.

Other related works include Tripakis [2002] who shows that diagnosability of transition systems represented as timed automata is PSPACE-complete. This result can be contrasted to the polynomial time result of Jiang et al. [2001] and our more tight NLOGSPACE-membership result in Theorem 4.1. More complex diagnosis problems for timed automata are investigated by Bouyer et al. [2005].

Wen et al. [2005] propose a polynomial time algorithm for testing diagnosability of transition systems represented as Petri nets. The algorithm tests for a sufficient but not necessary condition for diagnosability, and is therefore incomplete. A variant of our Theorem 4.4 shows that, assuming PSPACE̸=P, the test cannot be made complete by strengthening it without losing the polynomial time property: the Turing machine simulation in the proof of Theorem 4.4 can be performed with Petri nets as well.

Acknowledgements

Many thanks to Sylvie Thi´ebaux for directing me to this research topic and to Alban Grastien for comments and tightening the upper bound in Theorem 3.6 by a factor of 2.

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.