M Batteux

T Prosvirnova

A Rauzy Mtp

Advances in the simplification of Fault Trees automatically generated from AltaRica 3.0 models

Advances in the simplification of Fault Trees automatically generated from AltaRica 3.0 models

Michel Batteux, Tatiana Prosvirnova, Antoine

INTRODUCTION

Risk analysis relies on models. These models have several important characteristics:

• They are event-oriented. The system under study changes of state when events, such as failure, hazard, repair and so on, occur.

• They are probabilistic. The exact moment of the occurrence of a failure is in essence unpredictable.

• They are discrete. States are represented by means of variables that take their values into finite, usually very small, domains.

The last characteristic is pragmatic: given the difficulty to design models and computational com-plexity of the calculation of indicators, discrete abstractions are a necessary tradeoff. Hence the role of Boolean algebra in Reliability, Availability, Maintainability, Safety engineering. The most widely used modeling formalisms such as Fault Trees, Block Diagrams and Event Trees rely on Boolean algebra. There are cases however where binary states are not sufficient. For instance, it is sometimes necessary to represent the level of degradation of a component, the quality of a signal, and so on. This kind of models can be easily represented with AltaRica 3.0 -a high level modeling language dedicated to safety analyses [START_REF] Prosvirnova | The altarica 3.0 project for model-based safety assessment[END_REF]. AltaRica 3.0 is at the core of the OpenAltaRica project 1 which aim is to develop a complete set of assessment tools for the language, including among others compilers to Fault Trees [START_REF] Prosvirnova | Automated generation of minimal cut sets from altarica 3.0 models[END_REF] and Markov Chains [START_REF] Brameret | Automated generation of partial markov chain from high level descriptions[END_REF], stochastic and stepwise simulators [START_REF] Aupetit | Improving performances of the altarica 3.0 stochastic simulator[END_REF].

In this article we study how the notion of prime implicants can be extended to finite domain calculus and how to encode it efficiently. The contribution of this article is thus multiple. First, we present how the notion of prime implicants can be extended to finite domain calculus. Second, we discuss the efficient implementation of finite domain calculus. Finally we show how these results can be applied to simplify Fault Trees, automatically generated from AltaRica 3.0 models.

The remainder of this article is organized as follows. Section 2 describes a motivating example. Section 3 presents a theoretical work about finite domain calculus and discusses its implementation. Section 4 shows the application of the finite domain calculus to the simplification of Fault Trees automatically generated from AltaRica 3.0 models. Section 5 presents some experimental results using the motivating example. Section 6 concludes this article.

MOTIVATING EXAMPLE

Consider a parametric block diagram use case (see Figure 1) with three parameters:

• s the number of blocks in series;

• p the number of parallel blocks;

• q the level of recursivity (depth).

These relatively simple but large safety models can be easily represented in AltaRica 3.0 and handled simply and efficiently by means of the Fault Tree compilation tool chain.

Note that without loosing the efficiency of the assessment, in AltaRica 3.0, it is possible to represent multi-state blocks, e.g. consider the quality of data with the values ok, lost or erroneous, or the level of degradation with the values ok, degraded or failed. This use case is both representative of a class of industrial models and parametric to show the scalability of the approach. We shall use it throughout the article to illustrate the advances in the simplification of Fault Trees.

FINITE DOMAIN CALCULUS

Definitions

Let Ξ = {X 1 , X 2 , . . . , X n } be a finite set of variables. Each X i takes its values into a finite domain (a finite set of constants) denoted as dom(X i ). The set of well formed formulas over Ξ is the smallest set such that:

• The two Boolean constants 0 (false) and 1 (true) are formulas.

• If X is a variable and c is a constant then X = c is a formula. Such a formula X = c is called a literal and makes only sense if c ∈ dom(X).

• If f and g are formulas, then so are f + g (disjunction), f * g (conjunction), and -f (negation).

We assume that the negation (-) has a higher priority than the conjunction ( * ), which has a higher priority than the disjunction (+).

A product is a set of literals interpreted as the conjunction of its elements. A product is said fundamental if it does not contain two literals built over the same variable. We shall consider only fundamental products. The empty product is denoted 1.

A minterm is a product that contains a literal for each variable of Ξ. As we shall see, minterms play a fundamental role in the finite domain calculus for they are the atoms of the underlying Boolean algebra.

A sum of products is a set of products interpreted as the disjunction of its elements. The empty sum of products is denoted 0.

A variable assignment of Ξ is a function σ : Ξ → dom(X 1 ) × dom(X 2 ) × . . . × dom(X n ), that associates to each variable X i its value from dom(X i ), i = 1, ..., n.

Let f and g be formulas and σ be a variable assignment over Ξ. The value of σ(f ) is calculated recursively as follows:

• σ(1) = 1, σ(0) = 0; • σ(X = c) = 1 if σ(X) = c and 0 otherwise; • σ(f + g) = max(σ(f ), σ(g)), σ(f * g) = min(σ(f ), σ(g)), σ(-f ) = 1 -σ(f ).
The variable assignment σ satisfies the formula f , if σ(f ) = 1, otherwise is falsifies it.

There is a one to one correspondence between minterms and variable assignments: the minterm p corresponds to the variable assignment σ if for each variable X ∈ Ξ, X = c ∈ p if and only if σ(X) = c.

Implication, Equivalence, Properties

Let Ξ = {X 1 , . . . , X n } be a finite set of finite domain variables. Let f and g be two formulas built over Ξ. f implies g, which is denoted as f ⇒ g, if any variable assignment that satisfies f satisfies g as well. f is equivalent to g, which we denote as f ⇔ g, if both f ⇒ g and g ⇒ f .

The usual properties of Boolean algebras hold for the finite domain calculus:

Neutral element: f + 0 ⇔ 0 + f ⇔ f and f * 1 ⇔ 1 * f ⇔ f Absorbing element: f + 1 ⇔ 1 + f ⇔ 1 and f * 0 ⇔ 0 * f ⇔ 0 Idempotence: f + f ⇔ f and f * f ⇔ f Commutativity: f + g ⇔ g + f and f * g ⇔ g * f Associativity: f + (g + h) ⇔ (f + g) + h and f * (g * h) ⇔ (f * g) * h Distributivity: f + (g * h) ⇔ f * g + f * h and f * (g + h) ⇔ (f + g) * (f + h) Double negation: --f ⇔ f de Morgan's law: -(f + g) ⇔ -f * -g and -(f * g) ⇔ -f * -g

Negation

The real difference between the propositional and finite domain calculi stands in the negation.

Let Ξ be a finite set of variables, let X be a variable from Ξ, and finally let c be a constant of dom(X). Then, -(X = c) ⇔ Σ d∈dom(X),d =c (X = d) Theorem 1 (Elimination of negations). : For any formula of the finite domain calculus, there exists an equivalent formula involving no negation.

Note that any formula is equivalent to the sum of minterms that satisfies it, which is a first way to demonstrate the theorem. A more syntactic proof consists in pushing negations down to literals, thanks to de Morgan's law, and then to transform negative literals as shown above.

Subsumption, Resolution

Let p and q be two products built over Ξ. We say that p subsumes q if q ⇒ p, i.e. if and only if any literal of p is also a literal of q.If p subsumes q, then p + q ⇔ p.

Let X be a variable of Ξ, let dom(X) = {c 1 , c 2 , . . . , c k } and let p 1 , . . . , p k be k products in which X does not show up. Let r be the product p 1 * p 2 * . . . * p k . Then the following implication holds:

(X = c 1 ) * p 1 + . . . + (X = c k ) * p k ⇒ r
The product r is called the resolvent of the products (X = c 1 ) * p 1 , . . . , (X = c k ) * p k .

In the case, where there is a product p j such that p j = r, then the following equivalent holds:

(X = c 1 ) * p 1 + . . . + (X = c k ) * p k ⇔ (X = c 1 ) * p 1 + . . . + (X = c j ) * p j + . . . + (X = c k ) * p k + r ⇔ (X = c 1 ) * p 1 + . . . + (X = c j ) * p j + . . . + (X = c k ) * p k + r

Shannon Normal Form

Let X be a variable of Ξ, let c be a constant of dom(X) and finally let f be a formula built over Ξ.

There exist two formulas f 1 and f 0 in which the atom (X = c) does not show up such that:

f ⇔ (X = c) * f 1 + f 0
The above representation is called the pivotal decomposition of f with the respect to X and c.

Assume we are given an (arbitrary) order < over the variables of Ξ and over the constants of the domain of the variables of Ξ. The set of formulas in Shannon Normal Form is defined inductively as follows:

• The two constants 0 and 1 are in Shannon Normal Form.

• If f and g are two formulas in Shannon Normal Form, X is a variable and c is a constant of dom(X), the formula

(X = c) * f + g is in Shannon Normal Form if -X does not show up in f , and
-for all literal (Y = d) showing up in g, ei- ther X < Y or X = Y and c < d.

Representation Theorem

Let Ξ be a finite set of finite domain variables. Let X be a variable of Ξ, let c be a constant of dom(X) and finally let f = (X = c) * f 1 + f 0 be a formula in Shannon Normal Form built over Ξ.

In the above representation we can assume without a loss of generality that:

• f 1 = 0 as (X = c) * 0 + f 0 ⇔ f 0 • f 0 = 1 as (X = c) * f 1 + 1 ⇔ 1
From now, we shall assume that these two simplification rules are systematically applied.

Theorem 2 (Representation). : for any formula of the finite domain calculus, there exists at least one equivalent formula in Shannon Normal Form.

In general, this equivalent formula is not unique. We shall see that two of the formulas that represent a given sum of products are of special interest: the first one can be interpreted as sum of disjoint products, the other one as the set of prime implicants. These two formulas are extremum in a sense we shall explain.

A formula in Shannon Normal Form can be interpreted as a sum of products. Namely,

• SumOfProducts[0] = 0; • SumOfProducts[1] = 1; • SumOfProducts[(X = c) * f + g] = {(X = c) * p; p ∈ SumOf P roducts[f ]} ∪ SumOf P roducts[g]
Theorem 3 (Sums-of-Products). : Shannon Normal Formulas one-to-one correspond with Sums-of-Products (for a given order of variables and constants).

Factors and cofactors

The factor and cofactor of a formula f with respect to a variable X, denoted respectively as f |X and f ∼ X, are syntactic operations that select respectively the products of f that contain X and the products of f that do not contain X. The factor f |X is defined recursively as follows:

• 0|X = 0 and 1|X = 1

• [(X = c) * f + g]|X = (X = c) * f + [g|X] • [(Y = c) * f + g]|X = 0 if X < Y • [(Y = c) * f + g]|X = (Y = c) * [f |X] + [g|X] if X > Y
The cofactor f ∼ X is defined recursively as follows:

• 0 ∼ X = 0 and 1 ∼ X = 1 • [(X = c) * f + g] ∼ X = g ∼ X • [(Y = c) * f + g] ∼ X = g if X < Y • [(Y = c) * f + g] ∼ X = (Y = c) * [f ∼ X] + [g ∼ X] if X > Y

Logical operations

Let Ξ be a finite set of finite domain variables. Let X and Y be two variables of Ξ with X < Y . Let c, d and e be three constants such that c, d ∈ dom(X) with c < d, and e ∈ dom(Y ).

Finally let f = (X = c) * f 1 + f 0 , g = (X = c) * g 1 + g 0 , h = (X = d) * h 1 + h 0 and I = (Y = e) * I 1 + I 0 be four formulas built over Ξ in Shannon Normal Form.
The following equivalences hold and they are used as recursive equations to perform logical operations on formulae in Shannon Normal Form:

• f + g ⇔ (X = c) * [f 1 + g 1 ] + [f 0 + g 0 ] • f + h ⇔ (X = c) * f 1 + [f 0 + h] • f + I ⇔ (X = c) * f 1 + [f 0 + I] • f * g ⇔ (X = c) * [f 1 * g 1 + f 1 * g 0 ∼ X + f 0 ∼ X * g 1 ] + [f 0 * g 0 ] • f * h ⇔ (X = c) * [f 1 * h1 + f 1 * g 0 ∼ X] + [f 0 * g] • f * I ⇔ (X = c) * f 1 + [f 0 * I] • -f ⇔ [Σ d∈Dom(X),d =c (X = d) * -g] + [-f * -g]

Subsumption

As we shall see, it is of interest to remove from a formula f all the products that are subsumed by a product of a formula g. This operation, denoted f ÷ g, can be defined by means of the following recursive equations. Let Ξ be a finite set of finite domain variables. Let X and Y be two variables of Ξ (X < Y ), let c, d and e be three constants such that c, d ∈ dom(X), c < d, and e ∈ dom(Y ). Then:

• f ÷ 0 = f , f ÷ 1 = 0, 0 ÷ g = 0 and 1 ÷ g = 1 • [(X = c) * f 1 + f 0 ] ÷ [(X = c) * g 1 + g 0 ] = (X = c) * [(f 1 ÷ g 1 ) ÷ g 0 ] + f 0 ÷ g 0 • [(X = c) * f 1 + f 0 ] ÷ [(X = d) * g 1 + g 0 ] = (X = c)[f 1 ÷ g 0 ] + f 0 ÷ g 0 • [(X = c) * f 1 + f 0 ] ÷ [(Y = e) * g 1 + g 0 ] = (X = c)[f 1 ÷ [(Y = e) * g 1 + g 0 ]] +f 0 ÷ [(Y = e) * g 1 + g 0 ] • [(X = d) * f 1 + f 0 ] ÷ [(X = c) * g 1 + g 0 ] = (X = c)[f 1 ÷ g 0 ] + f 0 ÷ g0 • [(Y = e) * f 1 + f 0 ] ÷ [(X = c) * g 1 + g 0 ] = [(Y = e) * f 1 + f 0 ] ÷ g 0

Prime implicants

Let Ξ be a finite set of finite domain variables with an order over variables and constants. Let f and p be respectively a formula and a product built over Ξ.

• p is an implicant of f if p ⇒ f .

• p is a prime implicant of f if it is an implicant of f and no strict sub-product (subsuming product) of p is.

The set of prime implicants of f is denoted

P I[f ].
Theorem 4 (Decomposition of Prime Implicants). : Let f be a formula in Shannon Normal Form. Then

f = (X = c 1 ) * f 1 + ((X = c 2 ) * f 2 + . . . + ((X = c k ) * f k + f 0 )) . . .)
for some constants c 1 , . . . , c k from dom(X) and some formulas f 1 , . . . , f k , f 0 in Shannon Normal Form in which X does not occur.

Let h = (f 1 * f 2 * . . . * f k ) + f 0 .
Then, the set of prime implicants of f denoted by P I[f ] are calculated as follows:

P I[f ] = {(X = c 1 ) * p; p ∈ P I[f i ] ÷ P I[h]} . . . ∪{(X = c k ) * p; p ∈ P I[f k ] ÷ P I[h]} ∪{P I[h]}
The decomposition theorem gives an algorithm to calculate for any formula f in Shannon Normal Form an equivalent formula h such that:

g = SumOf P roducts[h] = P I[f ]
Because all possible resolutions and subsumptions have been performed, g can be considered as the most simplified form of f .

At the opposite, we may want to transform f into an equivalent sum of disjoint products so to be able to calculate the exact probability of f. Disjoining products encoded by f is performed by the dual operation of calculating resolvents.

Let

f = (X = c 1 ) * f 1 + ((X = c 2 ) * f 2 + . . . + ((X = c k ) * f k + f 0 )) . . .). Assume that dom(X) = {c 1 , . . . , c k } (if some constant c i of dom(X)
is missing we can always add the term (X = c i ) * 0). Then, f is equivalent to the following formula:

g = (X = c 1 ) * [f + f 0 ] + ((X = c 2 ) * [f 2 + f 0 ] + . . . + ((X = c k ) * [f k + f 0 )] + 0) . . .).
By applying this transformation recursively, we get a sum of disjoint products, which is also unique, for a given order on variables and constants.

Diagrammatic Representation

The idea is to represent sums of products in Shannon Normal Form by means of a variant of Bryant's Binary Decision Diagrams [START_REF] Bryant | Symbolic boolean manipulation with ordered binary-decision diagrams[END_REF]). The idea is therefore to represent formulas in Shannon Normal Form by means of Directed Acyclic Graphs with two types of nodes:

• Leaves, that are labeled with either 0 or 1.

• Internal nodes, that are labeled with a variable X and a constant c of dom(X) and that have two out-edges called the 1-outedge and the 0outedge. Such a node represents the formula (X = c) * f + g, where f and g are the formulas represented respectively by the node pointed by the 1-outedge and the node pointed by the 0outedge.

The Shannon Diagram representing a formula is always built bottom-up. Nodes are maintained into a unique table (and accessed by means of a hashtable ). In this way, for any formula f , there is at most one node representing f in the table. Checking the equivalence of two formulas is thus performed in constant time once their Shannon Diagrams are built.

APPLICATION

One of the possible applications of the finite domain calculus presented above is the simplification of Fault Trees automatically generated from AltaRica 3.0 models. AltaRica 3.0 is an event-based high level modeling language dedicated to Safety Analyses [START_REF] Prosvirnova | The altarica 3.0 project for model-based safety assessment[END_REF]. Its semantics is based on Guarded Transition Systems [START_REF] Rauzy | Guarded transition systems: a new states/events formalism for reliability studies[END_REF].

Guarded Transition Systems

A Guarded Transition System (GTS) G is a quintuple V, E, T, A, ι , where:

• V = S F is a set of variables, divided into two disjoint sets: a set S of state variables and a set F of flow variables.

• E is a set of events.

• T is a set of transitions. A transition is a triple t = e, G, P , where e is an event from E, G is a Boolean expression built over variables from V and called the guard of the transition, and P is an instruction built over V and called the action or the post-condition of the transition.

• A is an assertion (i.e. an instruction built over V ).

• ι is the initial (or default) assignment of variables of V .

A GTS G = V, E, T, A, ι is an implicit representation of a labeled Kripke structure, i.e. a graph Γ = (Σ, Θ), where

• the set of nodes Σ represent the variable assignments (of V ), and

• Θ is the set of edges labeled by the events from E.

Instructions of GTS are defined recursively as follows:

• "skip" is an empty instruction.

• If v is a variable and Exp an expression, then "v := Exp" is an instruction (called "assignment").

• If C is a Boolean expression, I is an instruction, then " if C then I" is an instruction (called "conditional assignment").

• If I 1 and I 2 are two instructions, then so is "I 1 ; I 2 " (called "parallel composition").

We shall consider two types of instructions. The "Actions" which are instructions in which left members of assignments are only state variables. The "Assertions" which are instructions in which left members of assignments are only flow variables.

Let denote by τ = P ropagate(A, ι, σ) a variable assignment obtained after applying the assertion A to the variable assignment σ., i.e. the calculation of flow

Compilation to Fault Trees

The compilation of AltaRica 3.0 models to Fault Trees works [START_REF] Prosvirnova | Automated generation of minimal cut sets from altarica 3.0 models[END_REF] in 5 steps (see Figure 2):

1. The AltaRica 3.0 model is flattened into a GTS.

The obtained GTS is partitioned into indepen-

dent GTSs plus an independent assertion.

3. Reachability graphs of each independent GTS are calculated.

4. Each reachability graph is separately compiled into Boolean equations.

The independent assertion is compiled into

Boolean equations.

The independent assertion V * , A * , ι * (the 5th step of the algorithm) is transformed into a set of Boolean formulas in the following way. For each pair (f, d), where f ∈ V * is a flow variable and d ∈ dom(f ) is its value, a formula φ (f,d) is constructed according to the instructions in the assertion A * and Boolean formulas {φ (u,c) , u ∈ U, c ∈ dom(u)} obtained from the compilation of the independent GTSs.

In order to compile the assertion into Boolean formulas efficiently, one need to separate it into independent parts. The dependency relation between variables in the assertion A * defines a dependency graph. This graph may contain cycles. The strongly connected components of this graph divide variables of A * into sets and enable to decompose the assertion A * into blocks of instructions A i (i = 1, ..., m), where m is the number of strongly connected components:

A * = A * 1 ; A * 2 ; . . . ; A * m Each block of instructions A * i is compiled into Boolean formulas recursively. Let denote by • V *
i -a set of variables labeling the vertices of the strongly connected component number i.

• A * i -an instruction that calculates the values of variables from

V * i . • ι * i -an initial assignment of variables from V * i . • W *
i -a set of variables such that variables from V * i depend on them in A * i . For all variable v in V * i the formula φ (v,c) (where c ∈ dom(v)) is built as follows: • Let φ σ be a product built over W * i (as defined in Section 3.1) calculated as follows:

• Let Σ = ×
φ σ = Π w∈W * i (w = σ(w)) • Let τ be a partial variable assignment, τ : V * i ∪ W * i → C, such that: ∀w ∈ W * i τ (w) = σ(w) •
The partial variable assignment τ can be completed by propagating the assertion A * i : τ = P ropagate(A * i , ι * i , τ ) • Then for each couple (v, c), with v ∈ V * i , such that τ (v) = c, the formula associated with (v, c) is updated as follows:

φ (v,c) ← φ (v,c) + φ σ
At the end of the algorithm, for all variables v ∈ V * and their values, we obtain a formula φ (v,c) built over a finite set of finite domain variables W * , such that v depends on them in the assertion A * . We use the diagrammic representation as defined in Section 3.11 to represent these formulas.

As we have seen in Section 3.10, φ (v,c) ⇔ P I[φ (v,c) ] and it is the most simplified form of φ (v,c) .

For each variable v ∈ V * and its value c ∈ dom(v), we compute P I[φ (v,c) ] and use this form, which greatly simplifies the generated Fault Tree.

Example

Consider the parametric block diagram use case presented in Section 2. Figure 3 illustrates how each basic block of these diagrams can be represented in Al-taRica 3.0.

The variable State represents the internal state of a basic block and takes its value in the domain BLOCKST AT E = {ok, ko}. A domain is an enumeration having any finite number of values. The

+ 0] + 0] f 1 = (B2.Out = ko) * 1 + [(B2.Out = ok) * 1 + 0] f 2 = (B2.Out = ko) * 1 + 0 f 0 = 0 h = f 1 * f 2 + f 0 = (B2.Out = ko) * 1 + 0 P I[h] = (B2.Out = ko) * 1 + 0 P I[f 1 ] = 1 P I[f 2 ] = (B2.Out = ko) * 1 + 0 P I[f 1 ] ÷ P I[h]

EXPERIMENTS

The Fault Tree compiler of the the OpenAltaRica platform produces Fault Trees from AltaRica 3.0 models. More precisely, according to one or several Boolean observers, representing safety cases of the modeled system, the Fault Tree compiler generates Fault Trees in Open-PSA model exchange format [START_REF] Hibti | Overview of the open psa platform[END_REF]) with these Boolean observers as top events. The produced Fault Trees can be then assessed by XFTA [START_REF] Rauzy | Anatomy of an efficient fault tree assessment engine[END_REF] to compute Minimal Cut Sets, probabilities of the top events, and so on.

We have implemented the algorithm presented in Section 4 and integrated it in the original version of the Fault Tree compiler. This algorithm greatly simplifies the generated Fault Trees, compared to those generated by the original version.

We have performed experiments with different values for the three parameters s, p and q of the motivating example pictured Figure 1.

In Table 1 we present the results obtained with the original version of the Fault Tree compiler and with the new one. The first column is the number of the considered cases. The five next columns, from the second column to the sixth column, present the number of components contained in each sub-parts. We start with n 1 parallel blocks, in each block there are n 2 sub-blocks in series, into each sub-block there are n 3 parallel subblocks, and so on. For example, the first case means 3 parallel blocks, with 3 sub-blocks in series, each one containing 3 parallel sub-blocks; whereas the fifth case means 2 blocks in series, with 4 parallel subblocks, each block containing 4 sub-blocks in series, with 4 parallel sub-blocks into each one. The seventh column represents the total number of basic blocks in the AltaRica 3.0 model. Finally, the eighth and ninth columns represent the number of intermediate events in the Fault Trees generated by the original version of the Fault Tree compiler (ninth column) and the new one (eighth column).

The main observation is about the benefit of the number of generated gates with the new version of the Fault Tree compiler in comparison to the original one. In average, this benefit is of 56.9%. It means that in average with the new algorithm, the number of generated gates is less than 56.9% compared to the number of generated gates with the original one. The minimal value is 37.8% in the second case; and the maximum value is 64.9% in the fifth case.

The benefit obtained with the new version of the algorithm implemented in the Fault Tree compiler is important.

CONCLUSION

Boolean models are widely used for probabilistic safety analysis. There are cases however where binary states are not sufficient. For instance, it is sometimes of interest to represent the level of degradation of a component, the quality of signal, and so on. This kind of models can be easily represented with AltaRica 3.0, a high level modeling language dedicated to safety analyses. AltaRica 3.0 comes with several efficient assessment tools, amongst them a Fault Tree compiler.

In this article we presented how the notion of prime implicants can be extended to finite domain calculus. We discussed how the finite domain calculus can be efficiently encoded using a variant of Binary Deci-sion Diagrams. We shown, using a parametric block diagram use case, how these results can be applied to simplify Fault Trees automatically generated from AltaRica 3.0 models. The number of generated intermediate events is on average divided by two, which greatly improves Fault Trees readability and the efficiency of their assessment.

Figure 1 :

 1 Figure 1: Parametric block diagram use case

Figure 2 :

 2 Figure 2: Compilation of AltaRica 3.0 models to Fault Trees

  be the Cartesian product of the domains of variables from W * i . • Let σ ∈ Σ be an assignment of variables from W * i .

Figure 3 :

 3 Figure 3: AltaRica 3.0 model of a basic block

Figure 4 :

 4 Figure 4: AltaRica 3.0 model of two blocks in series

Figure 5 :

 5 Figure 5: Diagrammatic representation of ((B1.Out = ok) * (B2.Out = ko) + (B1.Out = ko) * (B2.Out = ok) + (B1.Out = ko) * (B2.Out = ko))

  = 1 P I[f 2 ] ÷ P I[h] = 0 P I[f ] = (B1.Out = ko) * 1 +[(B2.Out = ko) * 1 + 0] which reads as (B1.Out = ko) + (B2.Out = ko). It is the most simplified form of φ (Out,ko) .

Table 1 :

 1 Parametric block diagram use case -fault tree compilation.

	Case	n 1	n 2	n 3	n 4	n 5	Number of blocks	Number of gates (new)	Number of gates (original)
	1 st	3	3	3	0	0	27	243	525
	2 nd	3	3	3	3	0	81	720	1158
	3 rd	4	4	4	0	0	64	537	1276
	4 th	4	4	4	4	0	256	2133	5114
	5 th	0	2	4	4	4	128	1135	3236
	6 th	0	3	3	3	2	54	558	1264
	7 th	0	3	3	3	0	27	243	596
	8 th	0	3	3	3	3	81	768	1914
	9 th	0	4	4	4	0	64	549	1562

See https://www.openaltarica.fr