RES for non-Markovian repairable fault trees
467
Notation. The nodes of a tree are given by nodes() = {0, 1, . . . , n − 1}. We
let v, w range over nodes(). A function type
: nodes() → {BE, SBE, AND, OR,
VOT k , PAND, SPARE, FDEP, RBOX} yields the type of each node in the tree. A
function chil
: nodes() → nodes()
∗ returns the ordered list of children of a
node. If clear from context, we omit the superscript from function names.
Semantics. Following [32] we give semantics to rft as Input/Output Stochastic Automata (iosa), so that we can handle arbitrary probability distributions.
Each state in the iosa represents a system configuration, indicating which components are operational and which have failed. Transitions among states describe
how the configuration changes when failures or repairs occur.
More precisely, a state in the iosa is a tuple x = (x 0 , . . . , x n−1 ) ∈ S ⊆ N
n ,
where S is the state space and x v denotes the state of node v in . The possible
values for x v depend on the type of v. The output z v ∈ {0, 1} of node v indicates
whether it is operational (z v =0) or failed (z v =1) and is calculated as follows:
– BEs (white circles in Fig. 1) have a binary state: x v = 0 if BE v is operational
and x v = 1 if it is failed. The output of a BE is its state: z v = x v .
– SBEs (gray circles in Fig. 1e) have two additional states: x v = 2, 3 if a
dormant SBE v is resp. operational, failed. Here z v = x v mod 2.
– ANDs have a binary state. Since the AND gate v fails iff all children fail:
x v = min w∈chil(v) z w . An AND gate outputs its internal state: z v = x v .
– OR gates are analogous to AND gates, but fail iff any child fail, i.e. z v =
x v = max w∈chil(v) z w for OR gate v.
– VOT gates also have a binary state: a VOT k gate fails iff 1 k m children
fail, thus z v = x v = 1 if k
w∈chil(v) z w , and z v = x v = 0 otherwise.
– PAND gates admit multiple states to represent the failure order of the children. For PAND v with two children we let x v equal: 0 if both children are
operational; 1 if the left child failed, but the right one has not; 2 if the right
child failed, but the left one has not; 3 if both children have failed, the right
one first; 4 if both children have failed, otherwise. The output of PAND gate
v is z v = 1 if x v = 4 and z v = 0 otherwise. PAND gates with more children
are handled by exploiting PAND(w 1 , w 2 , w 3 ) = PAND(PAND(w 1 , w 2 ), w 3 ).
– SPARE gate v leftmost input is its primary BE. All other (spare) inputs are
SBEs. SBEs can be shared among SPARE gates. When the primary of v fails,
it is replaced with an available SBE. An SBE is unavailable if it is failed, or if
it is replacing the primary BE of another SPARE. The output of v is z v = 1
if its primary is failed and no spare is available. Else z v = 0.
– An FDEP gate has no output. All inputs are BEs and the leftmost is the
trigger. We consider non-destructive FDEPs [7]: if the trigger fails, the output
of all other BE is set to 1, without affecting the internal state. Since this can
be modelled by a suitable combination of OR gates [32], we omit the details.
For example, the rft from Fig. 2 starts with all operational elements, so the
initial state is x
0 = (0, 0, 2, 0, 0). If then P fails, x P and z P are set to 1 (failed)
and S becomes x S = 0 (active and operational spare), so the state changes to
x
1 = (0, 1, 0, 0, 0). The traces of the iosa are given by x
0
x
1
· · · x
n
∈ S
∗ , where
a change from x
j to x
j+1 corresponds to transitions triggered in the iosa.
467
Notation. The nodes of a tree are given by nodes() = {0, 1, . . . , n − 1}. We
let v, w range over nodes(). A function type
: nodes() → {BE, SBE, AND, OR,
VOT k , PAND, SPARE, FDEP, RBOX} yields the type of each node in the tree. A
function chil
: nodes() → nodes()
∗ returns the ordered list of children of a
node. If clear from context, we omit the superscript from function names.
Semantics. Following [32] we give semantics to rft as Input/Output Stochastic Automata (iosa), so that we can handle arbitrary probability distributions.
Each state in the iosa represents a system configuration, indicating which components are operational and which have failed. Transitions among states describe
how the configuration changes when failures or repairs occur.
More precisely, a state in the iosa is a tuple x = (x 0 , . . . , x n−1 ) ∈ S ⊆ N
n ,
where S is the state space and x v denotes the state of node v in . The possible
values for x v depend on the type of v. The output z v ∈ {0, 1} of node v indicates
whether it is operational (z v =0) or failed (z v =1) and is calculated as follows:
– BEs (white circles in Fig. 1) have a binary state: x v = 0 if BE v is operational
and x v = 1 if it is failed. The output of a BE is its state: z v = x v .
– SBEs (gray circles in Fig. 1e) have two additional states: x v = 2, 3 if a
dormant SBE v is resp. operational, failed. Here z v = x v mod 2.
– ANDs have a binary state. Since the AND gate v fails iff all children fail:
x v = min w∈chil(v) z w . An AND gate outputs its internal state: z v = x v .
– OR gates are analogous to AND gates, but fail iff any child fail, i.e. z v =
x v = max w∈chil(v) z w for OR gate v.
– VOT gates also have a binary state: a VOT k gate fails iff 1 k m children
fail, thus z v = x v = 1 if k
w∈chil(v) z w , and z v = x v = 0 otherwise.
– PAND gates admit multiple states to represent the failure order of the children. For PAND v with two children we let x v equal: 0 if both children are
operational; 1 if the left child failed, but the right one has not; 2 if the right
child failed, but the left one has not; 3 if both children have failed, the right
one first; 4 if both children have failed, otherwise. The output of PAND gate
v is z v = 1 if x v = 4 and z v = 0 otherwise. PAND gates with more children
are handled by exploiting PAND(w 1 , w 2 , w 3 ) = PAND(PAND(w 1 , w 2 ), w 3 ).
– SPARE gate v leftmost input is its primary BE. All other (spare) inputs are
SBEs. SBEs can be shared among SPARE gates. When the primary of v fails,
it is replaced with an available SBE. An SBE is unavailable if it is failed, or if
it is replacing the primary BE of another SPARE. The output of v is z v = 1
if its primary is failed and no spare is available. Else z v = 0.
– An FDEP gate has no output. All inputs are BEs and the leftmost is the
trigger. We consider non-destructive FDEPs [7]: if the trigger fails, the output
of all other BE is set to 1, without affecting the internal state. Since this can
be modelled by a suitable combination of OR gates [32], we omit the details.
For example, the rft from Fig. 2 starts with all operational elements, so the
initial state is x
0 = (0, 0, 2, 0, 0). If then P fails, x P and z P are set to 1 (failed)
and S becomes x S = 0 (active and operational spare), so the state changes to
x
1 = (0, 1, 0, 0, 0). The traces of the iosa are given by x
0
x
1
· · · x
n
∈ S
∗ , where
a change from x
j to x
j+1 corresponds to transitions triggered in the iosa.