# Design of Logic Controllers Thanks to Symbolic Computation of Simultaneously Asserted Boolean Equations

Authors: Jean-Marc Roussel; Jean-Jacques Lesage
Journal: Mathematical Problems in Engineering
 (2014)

---

## Abstract

Formal methods can strongly contribute to improve dependability of controllers during design, by providing means to avoid flaws due to designers' omissions or specifications misinterpretations. This paper presents a synthesis method dedicated to logic controllers. Its goal is to obtain the control laws from specifications given in natural language by symbolic computation. The formal framework that underlies this method is the Boolean algebra ofn-variable switching functions. In this algebra, thanks to relations and theorems presented in this paper, it is possible to formally express logical controllers specifications, to automatically detect inconsistencies in specifications, and to obtain automatically the set of solutions or to choose an optimal solution according to given optimization criteria. The application of this synthesis method to an example allows illustrating its main advantages.


---

## Body

## 1. Introduction

Programmable logic controllers (PLCs) are industrial automation components that receive input signals coming from sensors and send output signals to actuators, in accordance with control laws implemented into a user program (Figure1). The control algorithms that allow the real time calculation of new output values, according to the current state of the PLC and the observation of new values of inputs, are written in standardized languages, such as ladder diagram (LD), structured text (ST) or instruction list (IL) [1]. A PLC cyclically performs three tasks: inputs reading, program execution, and outputs updating. The period of this task may be constant (periodic scan) or may vary (cyclic scan).Figure 1
PLC basic principle.Because of their reliability, even in very severe conditions in terms of temperature, vibrations, electromagnetic perturbations, and so forth, PLCs are frequently used for the control of safety-critical systems (energy production, transport, chemical industry, etc.). In this context, improving the reliability of the user program has been one of the main challenges of the past two decades in the field of automation. Among the different techniques that can be used in this aim [2], formal verification and validation and formal synthesis are the most efficient. Verification is the proof that the internal semantics of a model is correct, independently from the modeled system. The searched properties of the models are stability, deadlock existence, and so on . The validation determines if the model agrees with the designer’s purpose [3]. Efficient validation/verification techniques of PLC programs [4], most often based on model-checking technique, have been proposed by researchers and are now widely used in industry [5], despite problems of state-space explosion that arise when treating large scale systems.Contrary to verification techniques that aim at proving, after a PLC program has been more or less correctly designed by an expert, that control laws are safe, automatic synthesis methods aim at systematically generating control laws which guarantee by construction the respect of expected safety properties. The avoidance of human errors during the design of controllers is one of the main reasons for which synthesis is a very important subject of research in the field of discrete event systems (DES) since the end of 80’s.Most part of recent works in this area are still based onto the Supervisory Control Theory (SCT) [6] and are aiming for the synthesis of asupervisor, and not directly to thecontroller of an automated system. Furthermore, the use of state models (Finite Automata, Petri Nets, etc.) and their composition for the construction of the models of the plant and of the specifications generates a complexity which remains problematic for the synthesis of a supervisor for complex systems [7]. It is therefore interesting to explore other ways for performing synthesis, such as algebraic approaches. In previous works, we proposed a method specifically developed to get the control laws that can be directly implemented into the controller [8]. We have chosen to synthesize these control laws under the form of recurrent Boolean equations because of the wide possibilities they offer for the formalization of safety requirements and for implementation.Nevertheless, whatever is the used synthesis method, one of the weak links of the automatic generation of the control laws is the step of formal transcription by the designer (within state models or algebraic expressions) of the informal requirements and safety properties the controller has to satisfy. In the case of SCT, some authors have proposed more or less generic approaches for the construction of the models of the plant [9] or of the specifications [10]. But in any case, the hypothesis that requirements can be inconsistent has never been taken into account. Unfortunately in the framework of industrial collaborations we have been able to verify that it is always the case. In this paper we show how, in consideration of specific hypotheses, it is possible to install a correction loop for helping the designer to formalize these requirements and so improving the synthesis method robustness to the lack of precision of the specifications.This paper is organized as follows. Some basics of algebraic synthesis given in Sections2 and 3 recall the main steps of our method. Section 4 presents the mathematical framework of our approach and new results that allow us to accept inconsistencies in specifications. The strategy we developed for making the synthesis more robust to the lack of consistency of the specifications is described in Section 5, thanks to a case study.


## 2. Problem Statement

Figure2 proposes a generic representation of a DES whose controller has p Boolean inputs (u
i), q Boolean outputs (y
j), and r Boolean state variables (x
l). Plant and controller are connected through a closed loop exchanging inputs and outputs signals. The state variables, needed for expressing sequential behaviors of the controller, are represented by internal variables.Figure 2
A sequential DES.The algebraic modeling of the control laws of the controller necessitates the definition of(
q
+
r
) switching functions of (
p
+
r
) variables. Even if this representation is very compact (the r Boolean state variables allow the representation of 2
r different states), the construction by hands of these switching functions is a very tedious and error-prone task [11]; the controller of Figure 2 admits 2
p inputs combinations can send 2
q outputs combinations and can express (
2
2
(
p
+
r
)
)
(
q
+
r
) sequential behaviors. That is the reason why algebraic modeling approaches have been replaced by methods based on state models since the middle of 50’s [12, 13]. Nevertheless, thanks to recent mathematical results obtained onto Boolean algebras [14, 15], the automatic algebraic synthesis of switching functions is now possible.In [16] an interesting approach for the systematic construction of a reactive program from its formal specification is proposed. In this work, the program synthesis is considered as a theorem proving activity. A program with input x and output y, specified by the formula φ
(
x
,
y
), is constructed as a byproduct of proving the theorem (
∀
x
)
(
∃
y
)
φ
(
x
,
y
). The specification φ
(
x
,
y
) characterizes the expected relation between the input x and the output y computed by the program. This approach is based on the observation that the formula (
∀
x
)
(
∃
y
)
φ
(
x
,
y
) is equivalent to the second-order formula (
∃
f
)
(
∀
x
)
φ
(
x
,
f
(
x
)
), stating the existence of a function f, such that φ
(
x
,
f
(
x
)
) holds for every x.This approach provides a conceptual framework for the rigorous derivation of a program from its formal specification. It has also been used to synthesize specifications under the form of finite automata from their linear temporal logic (LTL) description [17].The core of our approach is based on this strategy: we aim at deducing the(
q
+
r
) switching functions of (
p
+
r
) variables which define the behavior of the controller from a formula φ
(
u
i
[
k
]
,
x
l
[
k
-
1
]
,
y
j
[
k
]
,
x
l
[
k
]
) that holds for every k, every u
i
[
k
], and every x
l
[
k
-
1
].To cope with combinatorial explosion, switching functions will be handled through a symbolic representation (and not their truth-tables which contain2
(
p
+
r
) Boolean values). Each input u
i (resp., output y
j) of the controller will be represented by a switching function U
i (resp., Y
j). To take into account the recursive aspect of state variables, each state variable x
l will be represented by two switching functions: X
l (for time [
k
]) and X
l
p (for time [
k
-
1
]).According to this representation, the synthesis of control laws of a logical system from its specification can now be transformed into the search of the solutions to the mathematical problem as follows:(1)
(
∀
U
i
)
(
∀
X
l
p
)
(
∃
Y
j
)
(
∃
X
l
)
φ
(
U
i
,
X
l
p
,
Y
j
,
X
l
)
,
where (
U
i
,
X
l
p
,
Y
j
,
X
l
) are (
p
+
q
+
2
r
) switching functions of (
p
+
r
) variables.


## 3. Overview of Our Method

The input data of the proposed method (Figure3) are unformal functional and safety requirements given by the designer. In practice, these requirements are most often given in a textual form and/or by using technical Taylor-made languages (Gantt diagrams, function blocks diagrams, Grafcet, etc.) or imposed standards.Figure 3
The algebraic synthesis method step by step.All the steps of our synthesis method are implemented into a prototype software tool developed in Python (Case studies are available online:http://www.lurpa.ens-cachan.fr/-226050.kjsp). The first step is the formalization of requirements within an algebraic description; examples are given in Section 5.2. Requirements expressed with a state model can directly be translated into recurrent Boolean equations, thanks to the algorithm proposed by Machado et al. [18]. In case where the knowhow of the designer enables him to build a priori the global form of the solution (or of a part of the whole solution) it is also possible to give fragments of solution as requirements [19].The second step consists in checking the consistency of the set of requirements by symbolic calculation. The sufficient condition for checking this consistency has been given in [20] but no strategy has been proposed for coping with potential inconsistencies. In this paper we show that thanks to new theorems the causes of these inconsistencies can be pointed out. It is then possible for the designer to fix priority rules between the concerned requirements that will allow finding, if exist, solutions despite inconsistencies.The core of the method is the third step, which consists in the synthesis of the control laws. This step is performed by solving the system of equations which represents the set of consistent requirements. The mathematical results we have obtained (Theorem12 given in Section 4.3), allow finding a parametric expression of the set of solutions.In the fourth step of the method, a particular solution has to be chosen among the set of solutions. For that, a specific value of each parameter of the general solution has to be fixed. In a previous work [19], we showed how well chosen heuristics can be used for fixing these parameters. In this paper, we show that the choice of a particular solution among the set of solutions can be expressed as an optimization problem. We propose new theorems that allow calculating the maximum and the minimum of a Boolean formula, and we show how optimal solutions can be automatically found. For ergonomic reasons, the synthesized control laws can finally be displayed under the form of a finite automaton [21].After the mathematical background of the method has been recalled, we are going to show how, in consideration of specific hypotheses, the second step of the method can be improved by a correction loop helping the designer to formalize the requirements and so improving the robustness of our synthesis method to the lack of precision of the specifications. The strategy to find an optimal solution according to given criteria will be also presented.


## 4. Mathematical Foundations

This section is composed of five subsections.  Sections4.1 and 4.2 recall some classical results about Boolean algebras and the Boolean algebra of n-variable switching functions. Section 4.3 presents how to solve Boolean equations. Sections 4.4 and 4.5 present specific results obtained for the algebraic synthesis of control laws.


### 4.1. Boolean Algebra: Typical Feature

Definition 1 (Boolean algebra).
(Definition 15.5 of [22]) Let B be a nonempty set that contains two special elements 0 (the zero element) and 1 (the unity, or one, element) and on which we define two closed binary operations +, ·, and an unary operation -. Then (
B
,
+
,
·
,
-
,
0,1
) is called a Boolean algebra if the following conditions are satisfied for all x
,
y
,
z
∈
B:
(2)
Commutative Laws:
x
+
y
=
y
+
x
x
·
y
=
y
·
x
Distributive Laws:
x
·
(
y
+
z
)
=
(
x
·
y
)
+
(
x
·
z
)
x
+
(
y
·
z
)
=
(
x
+
y
)
·
(
x
+
z
)
Identity Laws:
x
+
0
=
x
x
·
1
=
x
Inverse Laws:
x
+
x
-
=
1
x
·
x
-
=
0
0
≠
1
.Many Boolean algebras could be defined. The most known are the two-element Boolean algebra:(
{
0,1
}
,
∨
,
∧
,
¬
,
0,1
) and the algebra of classes (set of subsets of a set S): (
2
S
,
∪
,
∩
,
-
,
∅
,
S
).Definition 2 (Boolean formula).
(From Section3.6 of [15]) ABoolean formula (or a Boolean expression) on B is any formula which represents a combination of members of B by the operations +, ·, or -.By construction, any Boolean formula onB represents one and only one member of B. Two Boolean formulae are equivalent if and only if they represent the same member of B. Later on, a Boolean formula F built with the members (
α
1
,
…
,
α
n
) of B is denoted F
(
α
1
,
…
,
α
n
).Theorem 3 (Boole’s expansion of a Boolean formula).
Let(
α
1
,
…
,
α
n
) be n members of B
∖
{
0,1
}. Any Boolean Formula F
(
α
1
,
…
,
α
n
) can be expanded as
(3)
F
(
α
1
,
…
,
α
n
)
=
F
0
(
α
2
,
…
,
α
n
)
·
α
1
¯
+
F
1
(
α
2
,
…
,
α
n
)
·
α
1
,
where F
0
(
α
2
,
…
,
α
n
) and F
1
(
α
2
,
…
,
α
n
) are Boolean formulae of only α
2
,
…
,
α
n. These two formulae can be directly obtained from F
(
α
1
,
…
,
α
n
) as follows:
(4)
F
0
(
α
2
,
…
,
α
n
)
=
F
(
α
1
,
…
,
α
n
)
|
α
1
←
0
=
F
(
0
,
α
2
,
…
,
α
n
)
F
1
(
α
2
,
…
,
α
n
)
=
F
(
α
1
,
…
,
α
n
)
|
α
1
←
1
=
F
(
1
,
α
2
,
…
,
α
n
)
.The relationequality is not the only defined relation on a Boolean algebra. It is also possible to define a partial order relation between members of B. This relation is calledInclusion-Relation in [15].Definition 4 (Inclusion-Relation).
(Definition 15.6 of [22].) If x
,
y
∈
B, define x
≤
y if and only if x
·
y
=
x.As Relation Inclusion is reflexive (x
≤
x), antisymmetric (if x
≤
y and y
≤
x, then x
=
y), and transitive (if x
≤
y and y
≤
z, then x
≤
z), this relation defines a partial order between members of B (Theorem 15.4 of [22]).Since in any Boolean algebra,x
·
y
=
x
⇔
x
·
y
-
=
0, we also have x
≤
y
⇔
x
·
y
-
=
0.Remark 5.
For the algebra of classes(
2
S
,
∪
,
∩
,
-
,
∅
,
S
), the Inclusion-Relation is the well-known relation ⊆ and we have: x
⊆
y
⇔
x
∩
y
=
x.Theorem 6 (reduction of a set of relations).
(Theorem 5.3.1 of [15].) Any set of simultaneously asserted relations built with the members (
α
1
,
…
,
α
n
) of B can be reduced to a single equivalent relation such as: F
(
α
1
,
…
,
α
n
)
=
0.To obtain this equivalent relation, it is necessary(i)
to rewrite each equality according to(5)
F
1
(
α
1
,
…
,
α
n
)
=
F
2
(
α
1
,
…
,
α
n
)
⟺
F
1
(
α
1
,
…
,
α
n
)
·
F
2
(
α
1
,
…
,
α
n
)
¯
+
F
1
(
α
1
,
…
,
α
n
)
¯
·
F
2
(
α
1
,
…
,
α
n
)
=
0
,
(ii)
to rewrite each inclusion according to(6)
F
1
(
α
1
,
…
,
α
n
)
≤
F
2
(
α
1
,
…
,
α
n
)
⟺
F
1
(
α
1
,
…
,
α
n
)
·
F
2
(
α
1
,
…
,
α
n
)
¯
=
0
,
(iii)
to group together rewritten equalities as follows:(7)
{
F
1
(
α
1
,
…
,
α
n
)
=
0
F
2
(
α
1
,
…
,
α
n
)
=
0
⟺
F
1
(
α
1
,
…
,
α
n
)
+
F
2
(
α
1
,
…
,
α
n
)
=
0
.


### 4.2. The Boolean Algebra ofn-Variable Switching Functions

To avoid confusion between Boolean variables and Boolean functions of Boolean variables, each Boolean variableb
i is denoted by b
b
i. The set of the two Boolean values 0
b and 1
b is denoted by B
=
{
0
b
,
1
b
}.Definition 7 (N-variable switching functions).
(From Section 3.11 of [15].) An n-variableswitching function is a mapping of the form
(8)
f
:
B
n
⟶
B
(
b
b
1
,
…
,
b
b
n
)
⟼
f
(
b
b
1
,
…
,
b
b
n
)
h
h
h
h
h
h
h
h
h
h
h
h
where
B
=
{
b
0
,
b
1
}
.The domain of an-variable switching function has 2
n elements and the codomain has 2 elements; hence, there are 2
2
n
n-variable switching functions. Let F
n
(
B
) be the set of the 2
2
n
n-variable switching functions.F
n
(
B
) contains (
n
+
2
) specific n-variable switching functions: the 2constant functions
(
0,1
) and the n
projection-functions (f
Proj
i). These functions are defined as follows:
(9)
0:


B
n
⟶
B
(
b
1
b
,
…
,
b
n
b
)
⟼
0
b
1:


B
n
⟶
B
(
b
1
b
,
…
,
b
n
b
)
⟼
1
b
f
Proj
i
:


B
n
⟶
B
(
b
b
1
,
…
,
b
n
b
)
⟼
b
i
b
,F
n
(
B
) can be equipped with three closed operations (two binary and one unary operations)
(10)
Op
.
+
:
F
n
(
B
)
2
⟶
F
n
(
B
)
(
f
,
g
)
⟼
f
+
g
Op
.
·
:
F
n
(
B
)
2
⟶
F
n
(
B
)
(
f
,
g
)
⟼
f
·
g
Op
.
-
:
F
n
(
B
)
⟶
F
n
(
B
)
f
⟼
f
-
,
where ∀
(
b
1
b
,
…
,
b
n
b
)
∈
B
n,
(11)
(
f
+
g
)
(
b
1
b
,
…
,
b
n
b
)
=
f
(
b
1
b
,
…
,
b
n
b
)
∨
g
(
b
1
b
,
…
,
b
n
b
)
,
(
f
·
g
)
(
b
1
b
,
…
,
b
n
b
)
=
f
(
b
1
b
,
…
,
b
n
b
)
∧
g
(
b
1
b
,
…
,
b
n
b
)
,
f
¯
(
b
b
1
,
…
,
b
n
b
)
=
¬
f
(
b
b
1
,
…
,
b
n
b
)
.(
F
n
(
B
)
,
+
,
·
,
-
,
0,1
) is a Boolean algebra [22]. Then, it is possible to write a Boolean formula of n-variable switching functions and relations between Boolean formula of n-variable switching functions. In the case of n-variable switching functions, relations Equality and Inclusion can also be presented as follows:(i)
f and g are equal (f
=
g) if and only if the columns of the truth-tables of f, g are exactly the same, that is, ∀
(
b
1
b
,
…
,
b
n
b
)
∈
B
n, f
(
b
b
1
,
…
,
b
n
b
)
=
g
(
b
1
b
,
…
,
b
n
b
).
(ii)
f is included into g
(
f
≤
g
) if and only if the value of g is always b
1 when the value of f is b
1, that is, ∀
(
b
b
1
,
…
,
b
n
b
)
∈
B
n, [
f
(
b
b
1
,
…
,
b
n
b
)
=
0
b
], or [
g
(
b
b
1
,
…
,
b
n
b
)
=
1
b
].Remark 8.
Eachn-variable switching function can be expressed as a composition of (
f
Proj
1
,
…
,
f
Proj
n
,
0,1
) by operations +
,
· and -.Therefore, the Boolean algebra(
F
n
(
B
)
,
+
,
·
,
-
,
0,1
) is a mathematical framework which allows composing and to comparing switching functions. Thanks to the results presented in the next subsection, this framework allows also solving Boolean equations systems of switching functions.


### 4.3. Solutions of Boolean Equations over Boolean AlgebraF
n
(
B
)

In [15], Brown explains that many problems in the application of Boolean algebra may be reduced to solving an equation of the form
(12)
f
(
X
)
=
0
,
over a Boolean algebra B. Formal procedures for producing solution of this equation were developed by Boole himself as a way to treat problems of logical inference. Boolean equations have been studied extensively since Boole’s initial work (a bibliography of nearly 400 sources is presented in [14]). These works concern essentially the two-element Boolean algebra (
{
0
b
,
1
b
}
,
∨
,
∧
,
¬
,
0
b
,
1
b
).In our case, we focus on the Boolean algebra ofn-variable switching functions F
n
(
B
). We consider a Boolean system composed of m relations among members of F
n
(
B
) for which k of them are considered as unknowns. Theorems presented in this section permit to solve any system of Boolean equations as it exists in a canonic form of a Boolean system of k unknowns and we are able to calculate solutions for this form.


#### 4.3.1. Canonic Form of a Boolean System ofk Unknowns over Boolean Algebra F
n
(
B
)

Consider the Boolean algebra ofn-variable switching functions (
F
n
(
B
)
,
+
,
·
,
-
,
0,1
).(i)
Let(
f
Proj
1
,
…
,
f
Proj
n
) be the n projection-functions of F
n
(
B
).
(ii)
Let(
x
1
,
…
,
x
k
) be k elements of F
n
(
B
) considered asunknowns.For notational convenience, we note “X
k” as the vector (
x
1
,
…
,
x
k
) of the k unknowns and “Proj” as the vector (
f
Proj
1
,
…
,
f
Proj
n
) of the n projection-functions of F
n
(
B
).Theorem 9 (reduction of a set of relations betweenn-variable switching functions).
Any set of simultaneously asserted relations of switching functions can be reduced to a single equivalent relation such as(13)
F
(
X
k
,
Proj
)
=
0
.This theorem comes from Theorem6.In order to be able to write a canonic form for a Boolean system ofk unknowns over Boolean algebra F
n
(
B
), we introduce the following notation: for x
∈
F
n
(
B
) and a
∈
{
0,1
}, x
a is defined by
(14)
x
0
=
x
¯
,
x
1
=
x
.
This notation is extended to vectors as follows: for X
k
=
(
x
1
,
…
,
x
k
)
∈
F
n
(
B
)
k and A
k
=
(
a
1
,
…
,
a
k
)
∈
{
0,1
}
k, X
k
A
k is defined by
(15)
X
k
A
k
=
∏
i
=
1
i
=
k
x
i
a
i
=
x
i
a
1
·
⋯
·
x
k
a
k
.Theorem 10 (canonic form of a Boolean equation).
Any Boolean equationE
q
(
X
k
,
P
r
o
j
)
=
0 can be expressed within the canonic form
(16)
∑
A
k
∈
{
0,1
}
k
Eq
(
A
k
,
Proj
)
·
X
k
A
k
=
0
,
where E
q
(
A
k
,
P
r
o
j
) (with A
k
∈
{
0,1
}
k) are the 2
k
d
i
s
c
r
i
m
i
n
a
n
t
s of E
q
(
X
k
,
P
r
o
j
)
=
0 according to X
k (the term of “discriminant” comes from [15]).This canonic form is obtained by expandingEq
(
X
k
,
Proj
) according to the k unknowns (
x
1
,
…
,
x
k
). For example, we have
(17)
Eq
(
x
,
Proj
)
=
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
,
Eq
(
x
1
,
x
2
,
Proj
)
=
Eq
(
0,0
,
Proj
)
·
x
1
¯
·
x
2
¯
+
Eq
(
0,1
,
Proj
)
·
x
1
¯
·
x
2
+
Eq
(
1,0
,
Proj
)
·
x
1
·
x
2
¯
+
Eq
(
1,1
,
Proj
)
·
x
1
·
x
2
.


#### 4.3.2. Solution of a Single-Unknown Equation overF
n
(
B
)

The following theorem has initially been demonstrated for the two-element Boolean algebra [14]. A generalization for all Boolean algebras can be found in [15], but no detailed demonstration is given. A new formalization of this theorem and its full demonstration are given below.Theorem 11 (solution of a single-unknown equation).
The Boolean equation overF
n
(
B
)
(18)
E
q
(
x
,
P
r
o
j
)
=
0
,
for which the canonic form is
(19)
E
q
(
0
,
P
r
o
j
)
·
x
¯
+
E
q
(
1
,
P
r
o
j
)
·
x
=
0
,
is consistent (i.e., has at least one solution) if and only if the following condition is satisfied:
(20)
E
q
(
0
,
P
r
o
j
)
·
E
q
(
1
,
P
r
o
j
)
=
0
.
In this case, a general form of the solutions is
(21)
x
=
E
q
(
0
,
P
r
o
j
)
+
p
·
E
q
(
1
,
P
r
o
j
)
¯
,
where p is an arbitrary parameter, that is, a freely-chosen member of F
n
(
B
).
This solution can also be expressed as(22)
x
=
E
q
(
1
,
P
r
o
j
)
¯
·
(
E
q
(
0
,
P
r
o
j
)
+
p
)
=
p
¯
·
E
q
(
0
,
P
r
o
j
)
+
p
·
E
q
(
1
,
P
r
o
j
)
¯
.Proof.
This theorem can be proved in four steps as follows:(a)
Equation (18) is consistent if and only if (20) is satisfied;
(b)
Equation (21) is a solution of (18) if (20) is satisfied;
(c)
each solution of (18) can be expressed as (21);
(d)
if (20) is satisfied, the three parametric forms proposed are equivalent.
Step (a) can be proved as follows: Equation (20) is a sufficient condition for (18) to admit solutions since x
=
Eq
(
0
,
Proj
) is an obvious solution of (18). Equation (20) is also a necessary condition as if (18) admits a solution, then (18) can be also expressed thanks to the consensus theorem as Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
+
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
=
0 and we have necessarily Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
=
0.
To prove Step (b), it is sufficient to substitute the expression forx from (21) into (18) and to use (20) as follows:
(23)
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
=
Eq
(
0
,
Proj
)
·
(
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
)
¯
+
Eq
(
1
,
Proj
)
·
(
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
-
)
=
Eq
(
0
,
Proj
)
·
Eq
(
0
,
Proj
)
-
·
(
p
·
Eq
(
1
,
Proj
)
¯
)
¯
+
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
·
Eq
(
1
,
Proj
)
-
=
0
+
0
+
0
=
0
.
To prove Step (c), it is sufficient to find one elementp of F
n
(
B
) for each solution for x of (18). Let us consider p defined by “p
=
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x” where x is a solution to (18). Then we have
(24)
{
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
=
0
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
=
0
p
=
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x
⟹
x
=
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
as(25)
x
=
1
·
x
=
(
+
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
Eq
(
0
,
Proj
)
+
Eq
(
1
,
Proj
)
+
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
)
·
x
=
Eq
(
0
,
Proj
)
·
x
+
Eq
(
1
,
Proj
)
·
x
+
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x
=
Eq
(
0
,
Proj
)
·
x
+
0
+
Eq
(
1
,
Proj
)
¯
·
(
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x
)
as
Eq
(
1
,
Proj
)
·
x
=
0
=
Eq
(
0
,
Proj
)
·
x
+
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
¯
·
p
as
Eq
(
0
,
Proj
)
·
x
¯
=
0
=
Eq
(
0
,
Proj
)
·
(
x
+
x
¯
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
.
To prove Step (d), it is sufficient to rewrite (21) in the two other forms by using (20) as follows:
(26)
x
=
1
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
(
Eq
(
1
,
Proj
)
+
Eq
(
1
,
Proj
)
¯
)
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
+
(
Eq
(
0
,
Proj
)
+
p
)
·
Eq
(
1
,
Proj
)
¯
=
0
+
Eq
(
1
,
Proj
)
¯
·
(
Eq
(
0
,
Proj
)
+
p
)
=
Eq
(
1
,
Proj
)
¯
·
(
Eq
(
0
,
Proj
)
+
p
)
,
x
=
1
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
(
p
+
p
¯
)
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
(
Eq
(
0
,
Proj
)
+
Eq
(
1
,
Proj
)
¯
)
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
(
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
+
Eq
(
1
,
Proj
)
¯
)
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
(
0
+
Eq
(
1
,
Proj
)
¯
)
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
.


#### 4.3.3. Solution ofk-Unknown Equations over F
n
(
B
)

The global result presented in the following theorem can be found in [14] or [15]. However, in these works, the solution is not expressed with a parametric form, but with intervals only. The formulation presented in this paper is more adapted to symbolic computation and is mandatory for practice optimization.Ak-unknown equation can be solved by solving successively k single-unknown equations. If we consider the k-unknown equation as a single-unknown equation of x
k, its consistence condition corresponds to a (
k
-
1
)-unknown equation. The process can be iterated until x
1. After substituting S
(
x
1
) for x
1 in the last equation, it is possible to find the solution for x
2. Then, it is sufficient to apply this procedure again (
k
-
2
) times to obtain successively the solutions S
(
x
3
) to S
(
x
k
).Theorem 12 (solution of ak-unknown equation).
The Boolean equation overF
n
(
B
)
(27)
E
q
0
(
X
k
,
P
r
o
j
)
=
0
is consistent (i.e., has at least one solution) if and only if the following condition is satisfied:
(28)
∏
A
k
∈
{
0,1
}
k
‍
E
q
0
(
A
k
,
P
r
o
j
)
=
0
.
If (28) is satisfied, (27) admits one or more k-tuple solutions (
S
(
x
1
)
,
…
,
S
(
x
k
)
) such each component S
(
x
i
) is defined by
(29)
S
(
x
i
)
=
∏
A
k
-
i
∈
{
0,1
}
k
-
i
‍
E
q
i
-
1
(
0
,
A
k
-
i
,
P
r
o
j
)
+
p
i
·
∏
A
k
-
i
∈
{
0,1
}
k
-
i
E
q
i
-
1
(
1
,
A
k
-
i
,
P
r
o
j
)
¯
,
with (i)
E
q
i
(
x
i
+
1
,
…
,
x
k
,
P
r
o
j
)
=
E
q
i
-
1
(
x
i
,
x
i
+
1
,
…
,
x
k
,
P
r
o
j
)
|
x
i
←
S
(
x
i
)
(ii)
p
i is anarbitrary parameter, that is, a freely-chosen member of F
n
(
B
).The full demonstration of this theorem cannot be given in this paper because of lack of space (a full demonstration by mathematical induction can be found in [8]). A description of the different steps of the proof and the detail of the principal steps are given below.Proof (elements of Proof).
Equation (27) can be solved by applying Theorems 3 and 11  k times according to the unknowns x
k to x
1 as follows.
According to Theorem3, (27) is equivalent to
(30)
Eq
0
(
X
k
-
1
,
0
,
Proj
)
·
x
k
¯
+
Eq
0
(
X
k
-
1
,
1
,
Proj
)
·
x
k
=
0
.
According to Theorem 11, (30) admits solutions in x
k if and only if
(31)
Eq
0
(
X
k
-
1
,
0
,
Proj
)
·
Eq
0
(
X
k
-
1
,
1
,
Proj
)
=
0
.
Equation (31) is an equation with (
k
-
1
) unknowns. Each term of (31) can be expanded according to x
k
-
1 and (31) can be written in the form
(32)
(
Eq
0
(
X
k
-
2
,
0,0
,
Proj
)
·
Eq
0
(
X
k
-
2
,
0,1
,
Proj
)
)
·
x
k
-
1
¯
+
(
Eq
0
(
X
k
-
2
,
1,0
,
Proj
)
·
Eq
0
(
X
k
-
2
,
1,1
,
Proj
)
)
·
x
k
-
1
=
0
.
According to Theorem 11, (32) admits solutions in x
k
-
1 if and only if
(33)
∏
A
2
∈
{
0,1
}
2
‍
Eq
0
(
X
k
-
2
,
A
2
,
Proj
)
=
0
.
Equation (33) is an equation with (
k
-
2
) unknowns. Each term of (33) can be expanded according to x
k
-
2 and (33) can be written in the form
(34)
(
∏
A
2
∈
{
0,1
}
2
‍
Eq
0
(
X
k
-
3
,
0
,
A
2
,
Proj
)
)
·
x
k
-
2
¯
+
(
∏
A
2
∈
{
0,1
}
2
‍
Eq
0
(
X
k
-
3
,
1
,
A
2
,
Proj
)
)
·
x
k
-
2
=
0
.
In the end, we obtain an equation of only one unknownx
1 defined by
(35)
(
∏
A
k
-
1
∈
{
0,1
}
k
-
1
‍
Eq
0
(
0
,
A
k
-
1
,
Proj
)
)
·
x
1
¯
+
(
∏
A
k
-
1
∈
{
0,1
}
k
-
1
‍
Eq
0
(
1
,
A
k
-
1
,
Proj
)
)
·
x
1
=
0
.
According to Theorem11, (35) admits solutions if and only if
(36)
∏
A
k
∈
{
0,1
}
k
‍
Eq
0
(
A
k
,
Proj
)
=
0
.
When (36) is satisfied, the k equations for x
1 to x
k admit solutions. Equation (27) is then coherent and admits solutions.
When (36) is satisfied, solutions of (35) for x
1 are
(37)
S
(
x
1
)
=
∏
A
k
-
1
∈
{
0,1
}
k
-
1
‍
Eq
0
(
0
,
A
k
-
1
,
Proj
)
+
p
1
·
∏
A
k
-
1
∈
{
0,1
}
k
-
1
Eq
0
(
1
,
A
k
-
1
,
Proj
)
¯
.
After substitutingS
(
x
1
) for x
1 into (27), we obtain a new equation Eq
1
(
x
2
,
…
,
x
k
,
Proj
)
=
0 involving the (
k
-
1
) unknowns (
x
2
,
…
,
x
k
), where
(38)
Eq
1
(
x
2
,
…
,
x
k
,
Proj
)
=
Eq
0
(
x
1
,
x
2
,
…
,
x
k
,
Proj
)
|
x
1
←
S
(
x
1
)
.
By applying the previous procedure, we can obtainS
(
x
2
) and Eq
2
(
x
3
,
…
,
x
k
,
Proj
). Then, it suffices to apply this procedure again (
k
-
2
) times to obtain successively solutions S
(
x
3
) to S
(
x
k
).It is important to note that the order in which unknowns are treated affects only the parametric form of thek-tuple solution. This is due to the fact that the same k-tuple solution can be represented with several distinct parametric forms.


#### 4.3.4. Partial Conclusions

Thanks to theorems presented above, it is possible to obtain a parametric representation of all the solutions of any set of simultaneously asserted relations withk unknowns, if a solution exists. In practice, due to the complexity of systems to be designed, proposed set of simultaneously asserted relations is generally inconsistent [23]. To simplify the work of the designer, we have proved complementary theorems to improve the robustness of our method to the lack of precision of the specifications (Section 4.4).When several solutions exist, the comparison of solutions according to a given criterion can be envisaged since the Boolean algebraF
n
(
B
) is equipped with a partial order. To simplify the work of the designer too, we have developed a method to calculate the best solutions according to one or several criteria (Section 4.5).


### 4.4. Theorems to Cope with Inconsistencies of Specifications

In practice, it is very difficult for a designer to specify the whole requirements of a complex system without inconsistencies. It is the reason why requirements given by the designer are often declared as inconsistent according to Theorem12. Since the inconsistency condition is a Boolean formula, it is possible to use it for the detection of the origin of inconsistencies. Two cases have to be considered as follows:(i)
Several requirements cannot be simultaneously respected. In this case, a hierarchy between requirements can be proposed in order to find a solution. The requirements which have the lower priority have to be corrected for becoming consistent with the requirements which have the higher priority. This strategy is based on Theorem14.
(ii)
The detected inconsistency refers to specific combinations of projection-functions for which the designer knows that they are impossible blocking the synthesis process, it is necessary to introduce new assumptions and to use Theorem13.Theorem 13 (solution of a Boolean equation according to an assumption among the projection-functions).
The following problem(39)
E
q
u
a
t
i
o
n
t
o
s
o
l
v
e
:
E
q
0
(
X
k
,
P
r
o
j
)
=
0
A
s
s
u
m
p
t
i
o
n
s
:
A
(
P
r
o
j
)
=
0
admits the same solutions as the following equation:
(40)
E
q
0
(
X
k
,
P
r
o
j
)
≤
A
(
P
r
o
j
)
.Proof.
According toA
(
Proj
)
=
0, Eq
0
(
X
k
,
Proj
)
=
0 can be rewritten as
(41)
{
Eq
0
(
X
k
,
Proj
)
=
0
A
(
Proj
)
=
0
⟺
A
(
Proj
)
+
Eq
0
(
X
k
,
Proj
)
=
0
⟺
A
(
Proj
)
+
A
(
Proj
)
¯
·
Eq
0
(
X
k
,
Proj
)
=
0
⟺
{
A
(
Proj
)
¯
·
Eq
0
(
X
k
,
Proj
)
=
0
A
(
Proj
)
=
0
⟺
{
Eq
0
(
X
k
,
Proj
)
≤
A
(
Proj
)
A
(
Proj
)
=
0
.
EquationA
(
Proj
)
¯
·
Eq
0
(
X
k
,
Proj
)
=
0 is consistent if and only if the following condition is true (Theorem 12):
(42)
A
(
Proj
)
¯
·
∏
A
k
∈
{
0,1
}
k
‍
Eq
0
(
A
k
,
Proj
)
=
0
.
By construction, this new condition is the subset of the initial condition (∏
A
k
∈
{
0,1
}
k
‍
Eq
0
(
A
k
,
Proj
)
=
0) for which the proposed assumption is satisfied. All the other terms have been removed.
If (42) is satisfied, (40) admits one or more k-tuple solutions where each component S
(
x
i
) is defined by
(43)
S
(
x
i
)
=
A
(
Proj
)
¯
·
(
∏
A
k
-
i
∈
{
0,1
}
k
-
i
‍
Eq
i
-
1
(
0
,
A
k
-
i
,
Proj
)
+
p
i
·
∏
A
k
-
i
∈
{
0,1
}
k
-
i
Eq
i
-
1
(
1
,
A
k
-
i
,
Proj
)
¯
)
+
A
(
Proj
)
·
p
i
.
As A
(
Proj
)
=
0, S
(
x
i
) can also be expressed as
(44)
S
(
x
i
)
=
∏
A
k
-
i
∈
{
0,1
}
k
-
i
‍
Eq
i
-
1
(
0
,
A
k
-
i
,
Proj
)
+
p
i
·
∏
A
k
-
i
∈
{
0,1
}
k
-
i
Eq
i
-
1
(
1
,
A
k
-
i
,
Proj
)
¯
.
When A
(
Proj
)
=
0 is satisfied, the solutions of (40) are also solution to E
q
0
(
X
k
,
Proj
)
=
0.Theorem 14 (Solution of a Boolean equation system according to a priority rule between requirements).
The following problem(45)
E
q
u
a
t
i
o
n
s
s
y
s
t
e
m
t
o
solve:
H
R
F
H
(
X
k
,
P
r
o
j
)
=
0
L
R
F
L
(
X
k
,
P
r
o
j
)
=
0
O
R
F
O
(
X
k
,
P
r
o
j
)
=
0
P
r
i
o
r
i
t
y
r
u
l
e
b
e
t
w
e
e
n
requirements:
H
R
≫
L
R
,
where(i)
F
H
(
X
k
,
P
r
o
j
)
=
0 is the formal expression of the requirements which have the higher priority (HR);
(ii)
F
L
(
X
k
,
P
r
o
j
)
=
0 is the formal expression of the requirements which have the lower priority (LR);
(iii)
F
O
(
X
k
,
P
r
o
j
)
=
0 is the formal expression of the others requirements (OR);
(iv)
H
R
≫
L
R is the priority rule between inconsistent requirements,admits the same solutions as the system of equations as follows:
(46)
F
H
(
X
k
,
P
r
o
j
)
=
0
F
L
(
X
k
,
P
r
o
j
)
≤
I
(
P
r
o
j
)
F
O
(
X
k
,
P
r
o
j
)
=
0
,
where I
(
P
r
o
j
) is the inconsistency condition between requirements “HR” and “LR”:
(47)
I
(
P
r
o
j
)
=
∏
A
k
∈
{
0,1
}
k
‍
(
F
H
(
A
k
,
P
r
o
j
)
+
F
L
(
A
k
,
P
r
o
j
)
)
.Proof.
Thanks to Theorem12, the inconsistency condition I
(
Proj
) between requirements “HR” and “LR” can be found by solving equation F
H
(
X
k
,
Proj
)
+
F
L
(
X
k
,
Proj
)
=
0. We have
(48)
I
(
Proj
)
=
∏
A
k
∈
{
0,1
}
k
‍
(
F
H
(
A
k
,
Proj
)
+
F
L
(
A
k
,
Proj
)
)
.
To remove the inconsistency between requirements “HR” and “LR” according to the priority rule “HR ≫ LR”, it is necessary to restrict the range of requirement “LR” to the part for which there is no inconsistency, that is, I
(
Proj
)
=
0. That is the case, when F
L
(
X
k
,
Proj
)
=
0 is replaced by F
L
(
X
k
,
Proj
)
≤
I
(
Proj
).
Thanks to Theorem12, (49) admits always one or more k-tuple solutions and it is impossible to find a less restrictive condition over requirement “LR”. 									(49)
F
H
(
X
k
,
Proj
)
=
0
F
L
(
X
k
,
Proj
)
≤
I
(
Proj
)
.


### 4.5. Optimal Solutions of Boolean Equations overF
n
(
B
)

The goal of this step is to be able to obtain automatically the parametric form of thek-tuples solutions of F
n
(
B
) which satisfy not only a given equation (Eq
(
X
k
,
Proj
)
=
0) of Boolean functions but also which maximize (or minimize) a Boolean formula of these Boolean functions (F
C
(
X
k
,
Proj
)) corresponding to the desired optimization criterion.Generally speaking, the search of the best solution tuples according to a given criterion when the space of solutions is composed of discrete values is a complex mathematical issue. It is sometimes necessary to make a side-by-side comparison of each solution in order to identify the best one. In our case, this exhaustive method which cannot be used asF
n
(
B
) is only provided by a partial order; two particular solutions cannot always be ordered between themselves.Nevertheless, it is possible to obtain the researched parametric form of thek-tuples thanks to the following results.(i)
When an equation between Boolean functions has one or more solution tuples inF
n
(
B
), every Boolean formula onto these Boolean functions can be rewritten thanks to only projection-functions of F
n
(
B
) and free parameters of F
n
(
B
) which are describing these solution tuples.
(ii)
Every Boolean formula expressed as a composition of projection-functions ofF
n
(
B
) and free parameters of F
n
(
B
) has a unique maximum and a unique minimum. These extrema can be expressed thanks to only projection-functions of F
n
(
B
).Hence it is then possible to rewrite the initial problem(50)
Problem
to
solve:
Eq
(
X
k
,
Proj
)
=
0
Optimization
Criterion:
Maximization
of
F
C
(
X
k
,
Proj
)
,
into a 2-equation system to solve
(51)
Eq
(
X
k
,
Proj
)
=
0
F
C
(
X
k
,
Proj
)
=
Max
⁡
{
X
k
∣
Eq
(
X
k
,
Proj
)
=
0
}
(
F
C
(
X
k
,
Proj
)
)
.


#### 4.5.1. Extrema of a Boolean Formula according to Freely Chosen Members ofF
n
(
B
)

Considering the Boolean algebra ofn-variable switching functions (
F
n
(
B
)
,
+
,
·
,
-
,
0,1
),(i)
let(
f
Proj
1
,
…
,
f
Proj
n
) be the n
projection-functions of F
n
(
B
);
(ii)
let(
p
1
,
…
,
p
k
) be k elements of F
n
(
B
) considered asfreely chosen members. Let “P
k” be the corresponding vector.Any formulaF
(
P
k
,
Proj
) for which P
k are freely chosen members of F
n
(
B
) defines a subset of F
n
(
B
). According to the relation ≤, elements of this subset can be compared. In this specific case, the subset defined by F
(
P
k
,
Proj
) admits a minimal element and a maximal element.Theorem 15 (minimum and maximum of a Boolean formula).
Any formula
F
(
P
k, Proj) for which P
k are freely chosen members of F
n
(
B
) admits a minimum and a maximum defined as follows:
(52)
Min
⁡
P
k
∈
F
n
(
B
)
k
(
F
(
P
k
,
Proj
)
)
=
∏
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
)
Max
⁡
P
k
∈
F
n
(
B
)
k
(
F
(
P
k
,
Proj
)
)
=
∑
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
)
,Proof.
To prove this theorem, it is necessary to establish that(1)
∏
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
) is a lower bound of F
(
P
k
,
Proj
);
(2)
It exists at least one specific combination ofP
k for which F
(
P
k
,
Proj
)
=
∏
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
);
(3)
∑
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
) is an upper bound of F
(
P
k
,
Proj
);
(4)
It exists at least one specific combination ofP
k for which F
(
P
k
,
Proj
)
=
∑
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
).Details of this proof can be found in [24].


#### 4.5.2. Optimization Problem

Considering the Boolean algebra ofn-variable switching functions (
F
n
(
B
)
,
+
,
·
,
-
,
0,1
),(i)
let(
f
Proj
1
,
…
,
f
Proj
n
) be the n
projection-functions of F
n
(
B
). Let “Proj” be the corresponding vector;
(ii)
Let(
x
1
,
…
,
x
k
) be k elements of F
n
(
B
) considered asunknowns. Let “X
k” be the corresponding vector;
(iii)
Let(
p
1
,
…
,
p
k
) be k elements of F
n
(
B
) considered asfreely chosen members. Let “P
k” be the corresponding vector.;
(iv)
LetEq
(
X
k
,
Proj
)
=
0 be the Boolean equation to solve;
(v)
LetF
C
(
X
k
,
Proj
) be the Boolean formula of the given criterion to optimize (maximization or minimization).The method we propose, to obtain the parametric form of thek-tuple of switching functions solution of Eq
(
X
k
,
Proj
)
=
0 according to a given optimization criterion F
C
(
X
k
,
Proj
) is composed of five steps as follows.(i)
The first step is to establish the parametric form of thek-tuple solution to Eq
(
X
k
,
Proj
)
=
0 only, thanks to Theorem 12.
(ii)
The second step is to establish the parametric form of the given optimization criterionF
C
(
X
k
,
Proj
) by substituting S
(
x
i
) for x
i. Let F
SC
(
P
k
,
Proj
) be the result of this substitution.
(iii)
The third step is to calculate the extremum ofF
SC
(
P
k
,
Proj
) according to Theorem 15. Let F
EC
(
Proj
) be the Boolean formula of this extremum.
(iv)
The fourth step is to replace the given criterion by the equivalent relation(53)
F
C
(
X
k
,
Proj
)
=
F
EC
(
Proj
)
.
(v)
The fifth step is to establish the parametric form of thek-tuple solution of the equivalent problem
(54)
Eq
(
X
k
,
Proj
)
=
0
F
Crit
(
X
k
,
Proj
)
=
F
ExtCrit
(
Proj
)
.


#### 4.5.3. Partial Conclusions

Thanks to theorems presented in this section, it is now possible to obtain a parametric representation of the optimal solutions according to a given criterion, of any set of simultaneously asserted relations withk unknowns if a solution exists.The proposed method also permits to associate simultaneously or sequentially several criteria.(i)
When several criteria are treated simultaneously, the optimization problem can admit no solution. That is the case when the given criteria are antagonist.
(ii)
When several criteria are treated sequentially, the obtained solutions satisfy the criteria with a given priority order. An example of optimization with several criteria treated sequentially is presented in the next section.


## 4.1. Boolean Algebra: Typical Feature

Definition 1 (Boolean algebra).
(Definition 15.5 of [22]) Let B be a nonempty set that contains two special elements 0 (the zero element) and 1 (the unity, or one, element) and on which we define two closed binary operations +, ·, and an unary operation -. Then (
B
,
+
,
·
,
-
,
0,1
) is called a Boolean algebra if the following conditions are satisfied for all x
,
y
,
z
∈
B:
(2)
Commutative Laws:
x
+
y
=
y
+
x
x
·
y
=
y
·
x
Distributive Laws:
x
·
(
y
+
z
)
=
(
x
·
y
)
+
(
x
·
z
)
x
+
(
y
·
z
)
=
(
x
+
y
)
·
(
x
+
z
)
Identity Laws:
x
+
0
=
x
x
·
1
=
x
Inverse Laws:
x
+
x
-
=
1
x
·
x
-
=
0
0
≠
1
.Many Boolean algebras could be defined. The most known are the two-element Boolean algebra:(
{
0,1
}
,
∨
,
∧
,
¬
,
0,1
) and the algebra of classes (set of subsets of a set S): (
2
S
,
∪
,
∩
,
-
,
∅
,
S
).Definition 2 (Boolean formula).
(From Section3.6 of [15]) ABoolean formula (or a Boolean expression) on B is any formula which represents a combination of members of B by the operations +, ·, or -.By construction, any Boolean formula onB represents one and only one member of B. Two Boolean formulae are equivalent if and only if they represent the same member of B. Later on, a Boolean formula F built with the members (
α
1
,
…
,
α
n
) of B is denoted F
(
α
1
,
…
,
α
n
).Theorem 3 (Boole’s expansion of a Boolean formula).
Let(
α
1
,
…
,
α
n
) be n members of B
∖
{
0,1
}. Any Boolean Formula F
(
α
1
,
…
,
α
n
) can be expanded as
(3)
F
(
α
1
,
…
,
α
n
)
=
F
0
(
α
2
,
…
,
α
n
)
·
α
1
¯
+
F
1
(
α
2
,
…
,
α
n
)
·
α
1
,
where F
0
(
α
2
,
…
,
α
n
) and F
1
(
α
2
,
…
,
α
n
) are Boolean formulae of only α
2
,
…
,
α
n. These two formulae can be directly obtained from F
(
α
1
,
…
,
α
n
) as follows:
(4)
F
0
(
α
2
,
…
,
α
n
)
=
F
(
α
1
,
…
,
α
n
)
|
α
1
←
0
=
F
(
0
,
α
2
,
…
,
α
n
)
F
1
(
α
2
,
…
,
α
n
)
=
F
(
α
1
,
…
,
α
n
)
|
α
1
←
1
=
F
(
1
,
α
2
,
…
,
α
n
)
.The relationequality is not the only defined relation on a Boolean algebra. It is also possible to define a partial order relation between members of B. This relation is calledInclusion-Relation in [15].Definition 4 (Inclusion-Relation).
(Definition 15.6 of [22].) If x
,
y
∈
B, define x
≤
y if and only if x
·
y
=
x.As Relation Inclusion is reflexive (x
≤
x), antisymmetric (if x
≤
y and y
≤
x, then x
=
y), and transitive (if x
≤
y and y
≤
z, then x
≤
z), this relation defines a partial order between members of B (Theorem 15.4 of [22]).Since in any Boolean algebra,x
·
y
=
x
⇔
x
·
y
-
=
0, we also have x
≤
y
⇔
x
·
y
-
=
0.Remark 5.
For the algebra of classes(
2
S
,
∪
,
∩
,
-
,
∅
,
S
), the Inclusion-Relation is the well-known relation ⊆ and we have: x
⊆
y
⇔
x
∩
y
=
x.Theorem 6 (reduction of a set of relations).
(Theorem 5.3.1 of [15].) Any set of simultaneously asserted relations built with the members (
α
1
,
…
,
α
n
) of B can be reduced to a single equivalent relation such as: F
(
α
1
,
…
,
α
n
)
=
0.To obtain this equivalent relation, it is necessary(i)
to rewrite each equality according to(5)
F
1
(
α
1
,
…
,
α
n
)
=
F
2
(
α
1
,
…
,
α
n
)
⟺
F
1
(
α
1
,
…
,
α
n
)
·
F
2
(
α
1
,
…
,
α
n
)
¯
+
F
1
(
α
1
,
…
,
α
n
)
¯
·
F
2
(
α
1
,
…
,
α
n
)
=
0
,
(ii)
to rewrite each inclusion according to(6)
F
1
(
α
1
,
…
,
α
n
)
≤
F
2
(
α
1
,
…
,
α
n
)
⟺
F
1
(
α
1
,
…
,
α
n
)
·
F
2
(
α
1
,
…
,
α
n
)
¯
=
0
,
(iii)
to group together rewritten equalities as follows:(7)
{
F
1
(
α
1
,
…
,
α
n
)
=
0
F
2
(
α
1
,
…
,
α
n
)
=
0
⟺
F
1
(
α
1
,
…
,
α
n
)
+
F
2
(
α
1
,
…
,
α
n
)
=
0
.


## 4.2. The Boolean Algebra ofn-Variable Switching Functions

To avoid confusion between Boolean variables and Boolean functions of Boolean variables, each Boolean variableb
i is denoted by b
b
i. The set of the two Boolean values 0
b and 1
b is denoted by B
=
{
0
b
,
1
b
}.Definition 7 (N-variable switching functions).
(From Section 3.11 of [15].) An n-variableswitching function is a mapping of the form
(8)
f
:
B
n
⟶
B
(
b
b
1
,
…
,
b
b
n
)
⟼
f
(
b
b
1
,
…
,
b
b
n
)
h
h
h
h
h
h
h
h
h
h
h
h
where
B
=
{
b
0
,
b
1
}
.The domain of an-variable switching function has 2
n elements and the codomain has 2 elements; hence, there are 2
2
n
n-variable switching functions. Let F
n
(
B
) be the set of the 2
2
n
n-variable switching functions.F
n
(
B
) contains (
n
+
2
) specific n-variable switching functions: the 2constant functions
(
0,1
) and the n
projection-functions (f
Proj
i). These functions are defined as follows:
(9)
0:


B
n
⟶
B
(
b
1
b
,
…
,
b
n
b
)
⟼
0
b
1:


B
n
⟶
B
(
b
1
b
,
…
,
b
n
b
)
⟼
1
b
f
Proj
i
:


B
n
⟶
B
(
b
b
1
,
…
,
b
n
b
)
⟼
b
i
b
,F
n
(
B
) can be equipped with three closed operations (two binary and one unary operations)
(10)
Op
.
+
:
F
n
(
B
)
2
⟶
F
n
(
B
)
(
f
,
g
)
⟼
f
+
g
Op
.
·
:
F
n
(
B
)
2
⟶
F
n
(
B
)
(
f
,
g
)
⟼
f
·
g
Op
.
-
:
F
n
(
B
)
⟶
F
n
(
B
)
f
⟼
f
-
,
where ∀
(
b
1
b
,
…
,
b
n
b
)
∈
B
n,
(11)
(
f
+
g
)
(
b
1
b
,
…
,
b
n
b
)
=
f
(
b
1
b
,
…
,
b
n
b
)
∨
g
(
b
1
b
,
…
,
b
n
b
)
,
(
f
·
g
)
(
b
1
b
,
…
,
b
n
b
)
=
f
(
b
1
b
,
…
,
b
n
b
)
∧
g
(
b
1
b
,
…
,
b
n
b
)
,
f
¯
(
b
b
1
,
…
,
b
n
b
)
=
¬
f
(
b
b
1
,
…
,
b
n
b
)
.(
F
n
(
B
)
,
+
,
·
,
-
,
0,1
) is a Boolean algebra [22]. Then, it is possible to write a Boolean formula of n-variable switching functions and relations between Boolean formula of n-variable switching functions. In the case of n-variable switching functions, relations Equality and Inclusion can also be presented as follows:(i)
f and g are equal (f
=
g) if and only if the columns of the truth-tables of f, g are exactly the same, that is, ∀
(
b
1
b
,
…
,
b
n
b
)
∈
B
n, f
(
b
b
1
,
…
,
b
n
b
)
=
g
(
b
1
b
,
…
,
b
n
b
).
(ii)
f is included into g
(
f
≤
g
) if and only if the value of g is always b
1 when the value of f is b
1, that is, ∀
(
b
b
1
,
…
,
b
n
b
)
∈
B
n, [
f
(
b
b
1
,
…
,
b
n
b
)
=
0
b
], or [
g
(
b
b
1
,
…
,
b
n
b
)
=
1
b
].Remark 8.
Eachn-variable switching function can be expressed as a composition of (
f
Proj
1
,
…
,
f
Proj
n
,
0,1
) by operations +
,
· and -.Therefore, the Boolean algebra(
F
n
(
B
)
,
+
,
·
,
-
,
0,1
) is a mathematical framework which allows composing and to comparing switching functions. Thanks to the results presented in the next subsection, this framework allows also solving Boolean equations systems of switching functions.


## 4.3. Solutions of Boolean Equations over Boolean AlgebraF
n
(
B
)

In [15], Brown explains that many problems in the application of Boolean algebra may be reduced to solving an equation of the form
(12)
f
(
X
)
=
0
,
over a Boolean algebra B. Formal procedures for producing solution of this equation were developed by Boole himself as a way to treat problems of logical inference. Boolean equations have been studied extensively since Boole’s initial work (a bibliography of nearly 400 sources is presented in [14]). These works concern essentially the two-element Boolean algebra (
{
0
b
,
1
b
}
,
∨
,
∧
,
¬
,
0
b
,
1
b
).In our case, we focus on the Boolean algebra ofn-variable switching functions F
n
(
B
). We consider a Boolean system composed of m relations among members of F
n
(
B
) for which k of them are considered as unknowns. Theorems presented in this section permit to solve any system of Boolean equations as it exists in a canonic form of a Boolean system of k unknowns and we are able to calculate solutions for this form.


### 4.3.1. Canonic Form of a Boolean System ofk Unknowns over Boolean Algebra F
n
(
B
)

Consider the Boolean algebra ofn-variable switching functions (
F
n
(
B
)
,
+
,
·
,
-
,
0,1
).(i)
Let(
f
Proj
1
,
…
,
f
Proj
n
) be the n projection-functions of F
n
(
B
).
(ii)
Let(
x
1
,
…
,
x
k
) be k elements of F
n
(
B
) considered asunknowns.For notational convenience, we note “X
k” as the vector (
x
1
,
…
,
x
k
) of the k unknowns and “Proj” as the vector (
f
Proj
1
,
…
,
f
Proj
n
) of the n projection-functions of F
n
(
B
).Theorem 9 (reduction of a set of relations betweenn-variable switching functions).
Any set of simultaneously asserted relations of switching functions can be reduced to a single equivalent relation such as(13)
F
(
X
k
,
Proj
)
=
0
.This theorem comes from Theorem6.In order to be able to write a canonic form for a Boolean system ofk unknowns over Boolean algebra F
n
(
B
), we introduce the following notation: for x
∈
F
n
(
B
) and a
∈
{
0,1
}, x
a is defined by
(14)
x
0
=
x
¯
,
x
1
=
x
.
This notation is extended to vectors as follows: for X
k
=
(
x
1
,
…
,
x
k
)
∈
F
n
(
B
)
k and A
k
=
(
a
1
,
…
,
a
k
)
∈
{
0,1
}
k, X
k
A
k is defined by
(15)
X
k
A
k
=
∏
i
=
1
i
=
k
x
i
a
i
=
x
i
a
1
·
⋯
·
x
k
a
k
.Theorem 10 (canonic form of a Boolean equation).
Any Boolean equationE
q
(
X
k
,
P
r
o
j
)
=
0 can be expressed within the canonic form
(16)
∑
A
k
∈
{
0,1
}
k
Eq
(
A
k
,
Proj
)
·
X
k
A
k
=
0
,
where E
q
(
A
k
,
P
r
o
j
) (with A
k
∈
{
0,1
}
k) are the 2
k
d
i
s
c
r
i
m
i
n
a
n
t
s of E
q
(
X
k
,
P
r
o
j
)
=
0 according to X
k (the term of “discriminant” comes from [15]).This canonic form is obtained by expandingEq
(
X
k
,
Proj
) according to the k unknowns (
x
1
,
…
,
x
k
). For example, we have
(17)
Eq
(
x
,
Proj
)
=
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
,
Eq
(
x
1
,
x
2
,
Proj
)
=
Eq
(
0,0
,
Proj
)
·
x
1
¯
·
x
2
¯
+
Eq
(
0,1
,
Proj
)
·
x
1
¯
·
x
2
+
Eq
(
1,0
,
Proj
)
·
x
1
·
x
2
¯
+
Eq
(
1,1
,
Proj
)
·
x
1
·
x
2
.


### 4.3.2. Solution of a Single-Unknown Equation overF
n
(
B
)

The following theorem has initially been demonstrated for the two-element Boolean algebra [14]. A generalization for all Boolean algebras can be found in [15], but no detailed demonstration is given. A new formalization of this theorem and its full demonstration are given below.Theorem 11 (solution of a single-unknown equation).
The Boolean equation overF
n
(
B
)
(18)
E
q
(
x
,
P
r
o
j
)
=
0
,
for which the canonic form is
(19)
E
q
(
0
,
P
r
o
j
)
·
x
¯
+
E
q
(
1
,
P
r
o
j
)
·
x
=
0
,
is consistent (i.e., has at least one solution) if and only if the following condition is satisfied:
(20)
E
q
(
0
,
P
r
o
j
)
·
E
q
(
1
,
P
r
o
j
)
=
0
.
In this case, a general form of the solutions is
(21)
x
=
E
q
(
0
,
P
r
o
j
)
+
p
·
E
q
(
1
,
P
r
o
j
)
¯
,
where p is an arbitrary parameter, that is, a freely-chosen member of F
n
(
B
).
This solution can also be expressed as(22)
x
=
E
q
(
1
,
P
r
o
j
)
¯
·
(
E
q
(
0
,
P
r
o
j
)
+
p
)
=
p
¯
·
E
q
(
0
,
P
r
o
j
)
+
p
·
E
q
(
1
,
P
r
o
j
)
¯
.Proof.
This theorem can be proved in four steps as follows:(a)
Equation (18) is consistent if and only if (20) is satisfied;
(b)
Equation (21) is a solution of (18) if (20) is satisfied;
(c)
each solution of (18) can be expressed as (21);
(d)
if (20) is satisfied, the three parametric forms proposed are equivalent.
Step (a) can be proved as follows: Equation (20) is a sufficient condition for (18) to admit solutions since x
=
Eq
(
0
,
Proj
) is an obvious solution of (18). Equation (20) is also a necessary condition as if (18) admits a solution, then (18) can be also expressed thanks to the consensus theorem as Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
+
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
=
0 and we have necessarily Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
=
0.
To prove Step (b), it is sufficient to substitute the expression forx from (21) into (18) and to use (20) as follows:
(23)
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
=
Eq
(
0
,
Proj
)
·
(
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
)
¯
+
Eq
(
1
,
Proj
)
·
(
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
-
)
=
Eq
(
0
,
Proj
)
·
Eq
(
0
,
Proj
)
-
·
(
p
·
Eq
(
1
,
Proj
)
¯
)
¯
+
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
·
Eq
(
1
,
Proj
)
-
=
0
+
0
+
0
=
0
.
To prove Step (c), it is sufficient to find one elementp of F
n
(
B
) for each solution for x of (18). Let us consider p defined by “p
=
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x” where x is a solution to (18). Then we have
(24)
{
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
=
0
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
=
0
p
=
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x
⟹
x
=
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
as(25)
x
=
1
·
x
=
(
+
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
Eq
(
0
,
Proj
)
+
Eq
(
1
,
Proj
)
+
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
)
·
x
=
Eq
(
0
,
Proj
)
·
x
+
Eq
(
1
,
Proj
)
·
x
+
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x
=
Eq
(
0
,
Proj
)
·
x
+
0
+
Eq
(
1
,
Proj
)
¯
·
(
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x
)
as
Eq
(
1
,
Proj
)
·
x
=
0
=
Eq
(
0
,
Proj
)
·
x
+
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
¯
·
p
as
Eq
(
0
,
Proj
)
·
x
¯
=
0
=
Eq
(
0
,
Proj
)
·
(
x
+
x
¯
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
.
To prove Step (d), it is sufficient to rewrite (21) in the two other forms by using (20) as follows:
(26)
x
=
1
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
(
Eq
(
1
,
Proj
)
+
Eq
(
1
,
Proj
)
¯
)
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
+
(
Eq
(
0
,
Proj
)
+
p
)
·
Eq
(
1
,
Proj
)
¯
=
0
+
Eq
(
1
,
Proj
)
¯
·
(
Eq
(
0
,
Proj
)
+
p
)
=
Eq
(
1
,
Proj
)
¯
·
(
Eq
(
0
,
Proj
)
+
p
)
,
x
=
1
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
(
p
+
p
¯
)
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
(
Eq
(
0
,
Proj
)
+
Eq
(
1
,
Proj
)
¯
)
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
(
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
+
Eq
(
1
,
Proj
)
¯
)
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
(
0
+
Eq
(
1
,
Proj
)
¯
)
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
.


### 4.3.3. Solution ofk-Unknown Equations over F
n
(
B
)

The global result presented in the following theorem can be found in [14] or [15]. However, in these works, the solution is not expressed with a parametric form, but with intervals only. The formulation presented in this paper is more adapted to symbolic computation and is mandatory for practice optimization.Ak-unknown equation can be solved by solving successively k single-unknown equations. If we consider the k-unknown equation as a single-unknown equation of x
k, its consistence condition corresponds to a (
k
-
1
)-unknown equation. The process can be iterated until x
1. After substituting S
(
x
1
) for x
1 in the last equation, it is possible to find the solution for x
2. Then, it is sufficient to apply this procedure again (
k
-
2
) times to obtain successively the solutions S
(
x
3
) to S
(
x
k
).Theorem 12 (solution of ak-unknown equation).
The Boolean equation overF
n
(
B
)
(27)
E
q
0
(
X
k
,
P
r
o
j
)
=
0
is consistent (i.e., has at least one solution) if and only if the following condition is satisfied:
(28)
∏
A
k
∈
{
0,1
}
k
‍
E
q
0
(
A
k
,
P
r
o
j
)
=
0
.
If (28) is satisfied, (27) admits one or more k-tuple solutions (
S
(
x
1
)
,
…
,
S
(
x
k
)
) such each component S
(
x
i
) is defined by
(29)
S
(
x
i
)
=
∏
A
k
-
i
∈
{
0,1
}
k
-
i
‍
E
q
i
-
1
(
0
,
A
k
-
i
,
P
r
o
j
)
+
p
i
·
∏
A
k
-
i
∈
{
0,1
}
k
-
i
E
q
i
-
1
(
1
,
A
k
-
i
,
P
r
o
j
)
¯
,
with (i)
E
q
i
(
x
i
+
1
,
…
,
x
k
,
P
r
o
j
)
=
E
q
i
-
1
(
x
i
,
x
i
+
1
,
…
,
x
k
,
P
r
o
j
)
|
x
i
←
S
(
x
i
)
(ii)
p
i is anarbitrary parameter, that is, a freely-chosen member of F
n
(
B
).The full demonstration of this theorem cannot be given in this paper because of lack of space (a full demonstration by mathematical induction can be found in [8]). A description of the different steps of the proof and the detail of the principal steps are given below.Proof (elements of Proof).
Equation (27) can be solved by applying Theorems 3 and 11  k times according to the unknowns x
k to x
1 as follows.
According to Theorem3, (27) is equivalent to
(30)
Eq
0
(
X
k
-
1
,
0
,
Proj
)
·
x
k
¯
+
Eq
0
(
X
k
-
1
,
1
,
Proj
)
·
x
k
=
0
.
According to Theorem 11, (30) admits solutions in x
k if and only if
(31)
Eq
0
(
X
k
-
1
,
0
,
Proj
)
·
Eq
0
(
X
k
-
1
,
1
,
Proj
)
=
0
.
Equation (31) is an equation with (
k
-
1
) unknowns. Each term of (31) can be expanded according to x
k
-
1 and (31) can be written in the form
(32)
(
Eq
0
(
X
k
-
2
,
0,0
,
Proj
)
·
Eq
0
(
X
k
-
2
,
0,1
,
Proj
)
)
·
x
k
-
1
¯
+
(
Eq
0
(
X
k
-
2
,
1,0
,
Proj
)
·
Eq
0
(
X
k
-
2
,
1,1
,
Proj
)
)
·
x
k
-
1
=
0
.
According to Theorem 11, (32) admits solutions in x
k
-
1 if and only if
(33)
∏
A
2
∈
{
0,1
}
2
‍
Eq
0
(
X
k
-
2
,
A
2
,
Proj
)
=
0
.
Equation (33) is an equation with (
k
-
2
) unknowns. Each term of (33) can be expanded according to x
k
-
2 and (33) can be written in the form
(34)
(
∏
A
2
∈
{
0,1
}
2
‍
Eq
0
(
X
k
-
3
,
0
,
A
2
,
Proj
)
)
·
x
k
-
2
¯
+
(
∏
A
2
∈
{
0,1
}
2
‍
Eq
0
(
X
k
-
3
,
1
,
A
2
,
Proj
)
)
·
x
k
-
2
=
0
.
In the end, we obtain an equation of only one unknownx
1 defined by
(35)
(
∏
A
k
-
1
∈
{
0,1
}
k
-
1
‍
Eq
0
(
0
,
A
k
-
1
,
Proj
)
)
·
x
1
¯
+
(
∏
A
k
-
1
∈
{
0,1
}
k
-
1
‍
Eq
0
(
1
,
A
k
-
1
,
Proj
)
)
·
x
1
=
0
.
According to Theorem11, (35) admits solutions if and only if
(36)
∏
A
k
∈
{
0,1
}
k
‍
Eq
0
(
A
k
,
Proj
)
=
0
.
When (36) is satisfied, the k equations for x
1 to x
k admit solutions. Equation (27) is then coherent and admits solutions.
When (36) is satisfied, solutions of (35) for x
1 are
(37)
S
(
x
1
)
=
∏
A
k
-
1
∈
{
0,1
}
k
-
1
‍
Eq
0
(
0
,
A
k
-
1
,
Proj
)
+
p
1
·
∏
A
k
-
1
∈
{
0,1
}
k
-
1
Eq
0
(
1
,
A
k
-
1
,
Proj
)
¯
.
After substitutingS
(
x
1
) for x
1 into (27), we obtain a new equation Eq
1
(
x
2
,
…
,
x
k
,
Proj
)
=
0 involving the (
k
-
1
) unknowns (
x
2
,
…
,
x
k
), where
(38)
Eq
1
(
x
2
,
…
,
x
k
,
Proj
)
=
Eq
0
(
x
1
,
x
2
,
…
,
x
k
,
Proj
)
|
x
1
←
S
(
x
1
)
.
By applying the previous procedure, we can obtainS
(
x
2
) and Eq
2
(
x
3
,
…
,
x
k
,
Proj
). Then, it suffices to apply this procedure again (
k
-
2
) times to obtain successively solutions S
(
x
3
) to S
(
x
k
).It is important to note that the order in which unknowns are treated affects only the parametric form of thek-tuple solution. This is due to the fact that the same k-tuple solution can be represented with several distinct parametric forms.


### 4.3.4. Partial Conclusions

Thanks to theorems presented above, it is possible to obtain a parametric representation of all the solutions of any set of simultaneously asserted relations withk unknowns, if a solution exists. In practice, due to the complexity of systems to be designed, proposed set of simultaneously asserted relations is generally inconsistent [23]. To simplify the work of the designer, we have proved complementary theorems to improve the robustness of our method to the lack of precision of the specifications (Section 4.4).When several solutions exist, the comparison of solutions according to a given criterion can be envisaged since the Boolean algebraF
n
(
B
) is equipped with a partial order. To simplify the work of the designer too, we have developed a method to calculate the best solutions according to one or several criteria (Section 4.5).


## 4.3.1. Canonic Form of a Boolean System ofk Unknowns over Boolean Algebra F
n
(
B
)

Consider the Boolean algebra ofn-variable switching functions (
F
n
(
B
)
,
+
,
·
,
-
,
0,1
).(i)
Let(
f
Proj
1
,
…
,
f
Proj
n
) be the n projection-functions of F
n
(
B
).
(ii)
Let(
x
1
,
…
,
x
k
) be k elements of F
n
(
B
) considered asunknowns.For notational convenience, we note “X
k” as the vector (
x
1
,
…
,
x
k
) of the k unknowns and “Proj” as the vector (
f
Proj
1
,
…
,
f
Proj
n
) of the n projection-functions of F
n
(
B
).Theorem 9 (reduction of a set of relations betweenn-variable switching functions).
Any set of simultaneously asserted relations of switching functions can be reduced to a single equivalent relation such as(13)
F
(
X
k
,
Proj
)
=
0
.This theorem comes from Theorem6.In order to be able to write a canonic form for a Boolean system ofk unknowns over Boolean algebra F
n
(
B
), we introduce the following notation: for x
∈
F
n
(
B
) and a
∈
{
0,1
}, x
a is defined by
(14)
x
0
=
x
¯
,
x
1
=
x
.
This notation is extended to vectors as follows: for X
k
=
(
x
1
,
…
,
x
k
)
∈
F
n
(
B
)
k and A
k
=
(
a
1
,
…
,
a
k
)
∈
{
0,1
}
k, X
k
A
k is defined by
(15)
X
k
A
k
=
∏
i
=
1
i
=
k
x
i
a
i
=
x
i
a
1
·
⋯
·
x
k
a
k
.Theorem 10 (canonic form of a Boolean equation).
Any Boolean equationE
q
(
X
k
,
P
r
o
j
)
=
0 can be expressed within the canonic form
(16)
∑
A
k
∈
{
0,1
}
k
Eq
(
A
k
,
Proj
)
·
X
k
A
k
=
0
,
where E
q
(
A
k
,
P
r
o
j
) (with A
k
∈
{
0,1
}
k) are the 2
k
d
i
s
c
r
i
m
i
n
a
n
t
s of E
q
(
X
k
,
P
r
o
j
)
=
0 according to X
k (the term of “discriminant” comes from [15]).This canonic form is obtained by expandingEq
(
X
k
,
Proj
) according to the k unknowns (
x
1
,
…
,
x
k
). For example, we have
(17)
Eq
(
x
,
Proj
)
=
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
,
Eq
(
x
1
,
x
2
,
Proj
)
=
Eq
(
0,0
,
Proj
)
·
x
1
¯
·
x
2
¯
+
Eq
(
0,1
,
Proj
)
·
x
1
¯
·
x
2
+
Eq
(
1,0
,
Proj
)
·
x
1
·
x
2
¯
+
Eq
(
1,1
,
Proj
)
·
x
1
·
x
2
.


## 4.3.2. Solution of a Single-Unknown Equation overF
n
(
B
)

The following theorem has initially been demonstrated for the two-element Boolean algebra [14]. A generalization for all Boolean algebras can be found in [15], but no detailed demonstration is given. A new formalization of this theorem and its full demonstration are given below.Theorem 11 (solution of a single-unknown equation).
The Boolean equation overF
n
(
B
)
(18)
E
q
(
x
,
P
r
o
j
)
=
0
,
for which the canonic form is
(19)
E
q
(
0
,
P
r
o
j
)
·
x
¯
+
E
q
(
1
,
P
r
o
j
)
·
x
=
0
,
is consistent (i.e., has at least one solution) if and only if the following condition is satisfied:
(20)
E
q
(
0
,
P
r
o
j
)
·
E
q
(
1
,
P
r
o
j
)
=
0
.
In this case, a general form of the solutions is
(21)
x
=
E
q
(
0
,
P
r
o
j
)
+
p
·
E
q
(
1
,
P
r
o
j
)
¯
,
where p is an arbitrary parameter, that is, a freely-chosen member of F
n
(
B
).
This solution can also be expressed as(22)
x
=
E
q
(
1
,
P
r
o
j
)
¯
·
(
E
q
(
0
,
P
r
o
j
)
+
p
)
=
p
¯
·
E
q
(
0
,
P
r
o
j
)
+
p
·
E
q
(
1
,
P
r
o
j
)
¯
.Proof.
This theorem can be proved in four steps as follows:(a)
Equation (18) is consistent if and only if (20) is satisfied;
(b)
Equation (21) is a solution of (18) if (20) is satisfied;
(c)
each solution of (18) can be expressed as (21);
(d)
if (20) is satisfied, the three parametric forms proposed are equivalent.
Step (a) can be proved as follows: Equation (20) is a sufficient condition for (18) to admit solutions since x
=
Eq
(
0
,
Proj
) is an obvious solution of (18). Equation (20) is also a necessary condition as if (18) admits a solution, then (18) can be also expressed thanks to the consensus theorem as Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
+
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
=
0 and we have necessarily Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
=
0.
To prove Step (b), it is sufficient to substitute the expression forx from (21) into (18) and to use (20) as follows:
(23)
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
=
Eq
(
0
,
Proj
)
·
(
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
)
¯
+
Eq
(
1
,
Proj
)
·
(
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
-
)
=
Eq
(
0
,
Proj
)
·
Eq
(
0
,
Proj
)
-
·
(
p
·
Eq
(
1
,
Proj
)
¯
)
¯
+
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
·
Eq
(
1
,
Proj
)
-
=
0
+
0
+
0
=
0
.
To prove Step (c), it is sufficient to find one elementp of F
n
(
B
) for each solution for x of (18). Let us consider p defined by “p
=
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x” where x is a solution to (18). Then we have
(24)
{
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
=
0
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
·
x
=
0
p
=
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x
⟹
x
=
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
as(25)
x
=
1
·
x
=
(
+
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
Eq
(
0
,
Proj
)
+
Eq
(
1
,
Proj
)
+
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
)
·
x
=
Eq
(
0
,
Proj
)
·
x
+
Eq
(
1
,
Proj
)
·
x
+
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x
=
Eq
(
0
,
Proj
)
·
x
+
0
+
Eq
(
1
,
Proj
)
¯
·
(
Eq
(
0
,
Proj
)
¯
·
Eq
(
1
,
Proj
)
¯
·
x
)
as
Eq
(
1
,
Proj
)
·
x
=
0
=
Eq
(
0
,
Proj
)
·
x
+
Eq
(
0
,
Proj
)
·
x
¯
+
Eq
(
1
,
Proj
)
¯
·
p
as
Eq
(
0
,
Proj
)
·
x
¯
=
0
=
Eq
(
0
,
Proj
)
·
(
x
+
x
¯
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
.
To prove Step (d), it is sufficient to rewrite (21) in the two other forms by using (20) as follows:
(26)
x
=
1
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
(
Eq
(
1
,
Proj
)
+
Eq
(
1
,
Proj
)
¯
)
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
+
(
Eq
(
0
,
Proj
)
+
p
)
·
Eq
(
1
,
Proj
)
¯
=
0
+
Eq
(
1
,
Proj
)
¯
·
(
Eq
(
0
,
Proj
)
+
p
)
=
Eq
(
1
,
Proj
)
¯
·
(
Eq
(
0
,
Proj
)
+
p
)
,
x
=
1
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
(
p
+
p
¯
)
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
(
Eq
(
0
,
Proj
)
+
Eq
(
1
,
Proj
)
¯
)
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
(
Eq
(
0
,
Proj
)
·
Eq
(
1
,
Proj
)
+
Eq
(
1
,
Proj
)
¯
)
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
(
0
+
Eq
(
1
,
Proj
)
¯
)
=
p
¯
·
Eq
(
0
,
Proj
)
+
p
·
Eq
(
1
,
Proj
)
¯
.


## 4.3.3. Solution ofk-Unknown Equations over F
n
(
B
)

The global result presented in the following theorem can be found in [14] or [15]. However, in these works, the solution is not expressed with a parametric form, but with intervals only. The formulation presented in this paper is more adapted to symbolic computation and is mandatory for practice optimization.Ak-unknown equation can be solved by solving successively k single-unknown equations. If we consider the k-unknown equation as a single-unknown equation of x
k, its consistence condition corresponds to a (
k
-
1
)-unknown equation. The process can be iterated until x
1. After substituting S
(
x
1
) for x
1 in the last equation, it is possible to find the solution for x
2. Then, it is sufficient to apply this procedure again (
k
-
2
) times to obtain successively the solutions S
(
x
3
) to S
(
x
k
).Theorem 12 (solution of ak-unknown equation).
The Boolean equation overF
n
(
B
)
(27)
E
q
0
(
X
k
,
P
r
o
j
)
=
0
is consistent (i.e., has at least one solution) if and only if the following condition is satisfied:
(28)
∏
A
k
∈
{
0,1
}
k
‍
E
q
0
(
A
k
,
P
r
o
j
)
=
0
.
If (28) is satisfied, (27) admits one or more k-tuple solutions (
S
(
x
1
)
,
…
,
S
(
x
k
)
) such each component S
(
x
i
) is defined by
(29)
S
(
x
i
)
=
∏
A
k
-
i
∈
{
0,1
}
k
-
i
‍
E
q
i
-
1
(
0
,
A
k
-
i
,
P
r
o
j
)
+
p
i
·
∏
A
k
-
i
∈
{
0,1
}
k
-
i
E
q
i
-
1
(
1
,
A
k
-
i
,
P
r
o
j
)
¯
,
with (i)
E
q
i
(
x
i
+
1
,
…
,
x
k
,
P
r
o
j
)
=
E
q
i
-
1
(
x
i
,
x
i
+
1
,
…
,
x
k
,
P
r
o
j
)
|
x
i
←
S
(
x
i
)
(ii)
p
i is anarbitrary parameter, that is, a freely-chosen member of F
n
(
B
).The full demonstration of this theorem cannot be given in this paper because of lack of space (a full demonstration by mathematical induction can be found in [8]). A description of the different steps of the proof and the detail of the principal steps are given below.Proof (elements of Proof).
Equation (27) can be solved by applying Theorems 3 and 11  k times according to the unknowns x
k to x
1 as follows.
According to Theorem3, (27) is equivalent to
(30)
Eq
0
(
X
k
-
1
,
0
,
Proj
)
·
x
k
¯
+
Eq
0
(
X
k
-
1
,
1
,
Proj
)
·
x
k
=
0
.
According to Theorem 11, (30) admits solutions in x
k if and only if
(31)
Eq
0
(
X
k
-
1
,
0
,
Proj
)
·
Eq
0
(
X
k
-
1
,
1
,
Proj
)
=
0
.
Equation (31) is an equation with (
k
-
1
) unknowns. Each term of (31) can be expanded according to x
k
-
1 and (31) can be written in the form
(32)
(
Eq
0
(
X
k
-
2
,
0,0
,
Proj
)
·
Eq
0
(
X
k
-
2
,
0,1
,
Proj
)
)
·
x
k
-
1
¯
+
(
Eq
0
(
X
k
-
2
,
1,0
,
Proj
)
·
Eq
0
(
X
k
-
2
,
1,1
,
Proj
)
)
·
x
k
-
1
=
0
.
According to Theorem 11, (32) admits solutions in x
k
-
1 if and only if
(33)
∏
A
2
∈
{
0,1
}
2
‍
Eq
0
(
X
k
-
2
,
A
2
,
Proj
)
=
0
.
Equation (33) is an equation with (
k
-
2
) unknowns. Each term of (33) can be expanded according to x
k
-
2 and (33) can be written in the form
(34)
(
∏
A
2
∈
{
0,1
}
2
‍
Eq
0
(
X
k
-
3
,
0
,
A
2
,
Proj
)
)
·
x
k
-
2
¯
+
(
∏
A
2
∈
{
0,1
}
2
‍
Eq
0
(
X
k
-
3
,
1
,
A
2
,
Proj
)
)
·
x
k
-
2
=
0
.
In the end, we obtain an equation of only one unknownx
1 defined by
(35)
(
∏
A
k
-
1
∈
{
0,1
}
k
-
1
‍
Eq
0
(
0
,
A
k
-
1
,
Proj
)
)
·
x
1
¯
+
(
∏
A
k
-
1
∈
{
0,1
}
k
-
1
‍
Eq
0
(
1
,
A
k
-
1
,
Proj
)
)
·
x
1
=
0
.
According to Theorem11, (35) admits solutions if and only if
(36)
∏
A
k
∈
{
0,1
}
k
‍
Eq
0
(
A
k
,
Proj
)
=
0
.
When (36) is satisfied, the k equations for x
1 to x
k admit solutions. Equation (27) is then coherent and admits solutions.
When (36) is satisfied, solutions of (35) for x
1 are
(37)
S
(
x
1
)
=
∏
A
k
-
1
∈
{
0,1
}
k
-
1
‍
Eq
0
(
0
,
A
k
-
1
,
Proj
)
+
p
1
·
∏
A
k
-
1
∈
{
0,1
}
k
-
1
Eq
0
(
1
,
A
k
-
1
,
Proj
)
¯
.
After substitutingS
(
x
1
) for x
1 into (27), we obtain a new equation Eq
1
(
x
2
,
…
,
x
k
,
Proj
)
=
0 involving the (
k
-
1
) unknowns (
x
2
,
…
,
x
k
), where
(38)
Eq
1
(
x
2
,
…
,
x
k
,
Proj
)
=
Eq
0
(
x
1
,
x
2
,
…
,
x
k
,
Proj
)
|
x
1
←
S
(
x
1
)
.
By applying the previous procedure, we can obtainS
(
x
2
) and Eq
2
(
x
3
,
…
,
x
k
,
Proj
). Then, it suffices to apply this procedure again (
k
-
2
) times to obtain successively solutions S
(
x
3
) to S
(
x
k
).It is important to note that the order in which unknowns are treated affects only the parametric form of thek-tuple solution. This is due to the fact that the same k-tuple solution can be represented with several distinct parametric forms.


## 4.3.4. Partial Conclusions

Thanks to theorems presented above, it is possible to obtain a parametric representation of all the solutions of any set of simultaneously asserted relations withk unknowns, if a solution exists. In practice, due to the complexity of systems to be designed, proposed set of simultaneously asserted relations is generally inconsistent [23]. To simplify the work of the designer, we have proved complementary theorems to improve the robustness of our method to the lack of precision of the specifications (Section 4.4).When several solutions exist, the comparison of solutions according to a given criterion can be envisaged since the Boolean algebraF
n
(
B
) is equipped with a partial order. To simplify the work of the designer too, we have developed a method to calculate the best solutions according to one or several criteria (Section 4.5).


## 4.4. Theorems to Cope with Inconsistencies of Specifications

In practice, it is very difficult for a designer to specify the whole requirements of a complex system without inconsistencies. It is the reason why requirements given by the designer are often declared as inconsistent according to Theorem12. Since the inconsistency condition is a Boolean formula, it is possible to use it for the detection of the origin of inconsistencies. Two cases have to be considered as follows:(i)
Several requirements cannot be simultaneously respected. In this case, a hierarchy between requirements can be proposed in order to find a solution. The requirements which have the lower priority have to be corrected for becoming consistent with the requirements which have the higher priority. This strategy is based on Theorem14.
(ii)
The detected inconsistency refers to specific combinations of projection-functions for which the designer knows that they are impossible blocking the synthesis process, it is necessary to introduce new assumptions and to use Theorem13.Theorem 13 (solution of a Boolean equation according to an assumption among the projection-functions).
The following problem(39)
E
q
u
a
t
i
o
n
t
o
s
o
l
v
e
:
E
q
0
(
X
k
,
P
r
o
j
)
=
0
A
s
s
u
m
p
t
i
o
n
s
:
A
(
P
r
o
j
)
=
0
admits the same solutions as the following equation:
(40)
E
q
0
(
X
k
,
P
r
o
j
)
≤
A
(
P
r
o
j
)
.Proof.
According toA
(
Proj
)
=
0, Eq
0
(
X
k
,
Proj
)
=
0 can be rewritten as
(41)
{
Eq
0
(
X
k
,
Proj
)
=
0
A
(
Proj
)
=
0
⟺
A
(
Proj
)
+
Eq
0
(
X
k
,
Proj
)
=
0
⟺
A
(
Proj
)
+
A
(
Proj
)
¯
·
Eq
0
(
X
k
,
Proj
)
=
0
⟺
{
A
(
Proj
)
¯
·
Eq
0
(
X
k
,
Proj
)
=
0
A
(
Proj
)
=
0
⟺
{
Eq
0
(
X
k
,
Proj
)
≤
A
(
Proj
)
A
(
Proj
)
=
0
.
EquationA
(
Proj
)
¯
·
Eq
0
(
X
k
,
Proj
)
=
0 is consistent if and only if the following condition is true (Theorem 12):
(42)
A
(
Proj
)
¯
·
∏
A
k
∈
{
0,1
}
k
‍
Eq
0
(
A
k
,
Proj
)
=
0
.
By construction, this new condition is the subset of the initial condition (∏
A
k
∈
{
0,1
}
k
‍
Eq
0
(
A
k
,
Proj
)
=
0) for which the proposed assumption is satisfied. All the other terms have been removed.
If (42) is satisfied, (40) admits one or more k-tuple solutions where each component S
(
x
i
) is defined by
(43)
S
(
x
i
)
=
A
(
Proj
)
¯
·
(
∏
A
k
-
i
∈
{
0,1
}
k
-
i
‍
Eq
i
-
1
(
0
,
A
k
-
i
,
Proj
)
+
p
i
·
∏
A
k
-
i
∈
{
0,1
}
k
-
i
Eq
i
-
1
(
1
,
A
k
-
i
,
Proj
)
¯
)
+
A
(
Proj
)
·
p
i
.
As A
(
Proj
)
=
0, S
(
x
i
) can also be expressed as
(44)
S
(
x
i
)
=
∏
A
k
-
i
∈
{
0,1
}
k
-
i
‍
Eq
i
-
1
(
0
,
A
k
-
i
,
Proj
)
+
p
i
·
∏
A
k
-
i
∈
{
0,1
}
k
-
i
Eq
i
-
1
(
1
,
A
k
-
i
,
Proj
)
¯
.
When A
(
Proj
)
=
0 is satisfied, the solutions of (40) are also solution to E
q
0
(
X
k
,
Proj
)
=
0.Theorem 14 (Solution of a Boolean equation system according to a priority rule between requirements).
The following problem(45)
E
q
u
a
t
i
o
n
s
s
y
s
t
e
m
t
o
solve:
H
R
F
H
(
X
k
,
P
r
o
j
)
=
0
L
R
F
L
(
X
k
,
P
r
o
j
)
=
0
O
R
F
O
(
X
k
,
P
r
o
j
)
=
0
P
r
i
o
r
i
t
y
r
u
l
e
b
e
t
w
e
e
n
requirements:
H
R
≫
L
R
,
where(i)
F
H
(
X
k
,
P
r
o
j
)
=
0 is the formal expression of the requirements which have the higher priority (HR);
(ii)
F
L
(
X
k
,
P
r
o
j
)
=
0 is the formal expression of the requirements which have the lower priority (LR);
(iii)
F
O
(
X
k
,
P
r
o
j
)
=
0 is the formal expression of the others requirements (OR);
(iv)
H
R
≫
L
R is the priority rule between inconsistent requirements,admits the same solutions as the system of equations as follows:
(46)
F
H
(
X
k
,
P
r
o
j
)
=
0
F
L
(
X
k
,
P
r
o
j
)
≤
I
(
P
r
o
j
)
F
O
(
X
k
,
P
r
o
j
)
=
0
,
where I
(
P
r
o
j
) is the inconsistency condition between requirements “HR” and “LR”:
(47)
I
(
P
r
o
j
)
=
∏
A
k
∈
{
0,1
}
k
‍
(
F
H
(
A
k
,
P
r
o
j
)
+
F
L
(
A
k
,
P
r
o
j
)
)
.Proof.
Thanks to Theorem12, the inconsistency condition I
(
Proj
) between requirements “HR” and “LR” can be found by solving equation F
H
(
X
k
,
Proj
)
+
F
L
(
X
k
,
Proj
)
=
0. We have
(48)
I
(
Proj
)
=
∏
A
k
∈
{
0,1
}
k
‍
(
F
H
(
A
k
,
Proj
)
+
F
L
(
A
k
,
Proj
)
)
.
To remove the inconsistency between requirements “HR” and “LR” according to the priority rule “HR ≫ LR”, it is necessary to restrict the range of requirement “LR” to the part for which there is no inconsistency, that is, I
(
Proj
)
=
0. That is the case, when F
L
(
X
k
,
Proj
)
=
0 is replaced by F
L
(
X
k
,
Proj
)
≤
I
(
Proj
).
Thanks to Theorem12, (49) admits always one or more k-tuple solutions and it is impossible to find a less restrictive condition over requirement “LR”. 									(49)
F
H
(
X
k
,
Proj
)
=
0
F
L
(
X
k
,
Proj
)
≤
I
(
Proj
)
.


## 4.5. Optimal Solutions of Boolean Equations overF
n
(
B
)

The goal of this step is to be able to obtain automatically the parametric form of thek-tuples solutions of F
n
(
B
) which satisfy not only a given equation (Eq
(
X
k
,
Proj
)
=
0) of Boolean functions but also which maximize (or minimize) a Boolean formula of these Boolean functions (F
C
(
X
k
,
Proj
)) corresponding to the desired optimization criterion.Generally speaking, the search of the best solution tuples according to a given criterion when the space of solutions is composed of discrete values is a complex mathematical issue. It is sometimes necessary to make a side-by-side comparison of each solution in order to identify the best one. In our case, this exhaustive method which cannot be used asF
n
(
B
) is only provided by a partial order; two particular solutions cannot always be ordered between themselves.Nevertheless, it is possible to obtain the researched parametric form of thek-tuples thanks to the following results.(i)
When an equation between Boolean functions has one or more solution tuples inF
n
(
B
), every Boolean formula onto these Boolean functions can be rewritten thanks to only projection-functions of F
n
(
B
) and free parameters of F
n
(
B
) which are describing these solution tuples.
(ii)
Every Boolean formula expressed as a composition of projection-functions ofF
n
(
B
) and free parameters of F
n
(
B
) has a unique maximum and a unique minimum. These extrema can be expressed thanks to only projection-functions of F
n
(
B
).Hence it is then possible to rewrite the initial problem(50)
Problem
to
solve:
Eq
(
X
k
,
Proj
)
=
0
Optimization
Criterion:
Maximization
of
F
C
(
X
k
,
Proj
)
,
into a 2-equation system to solve
(51)
Eq
(
X
k
,
Proj
)
=
0
F
C
(
X
k
,
Proj
)
=
Max
⁡
{
X
k
∣
Eq
(
X
k
,
Proj
)
=
0
}
(
F
C
(
X
k
,
Proj
)
)
.


### 4.5.1. Extrema of a Boolean Formula according to Freely Chosen Members ofF
n
(
B
)

Considering the Boolean algebra ofn-variable switching functions (
F
n
(
B
)
,
+
,
·
,
-
,
0,1
),(i)
let(
f
Proj
1
,
…
,
f
Proj
n
) be the n
projection-functions of F
n
(
B
);
(ii)
let(
p
1
,
…
,
p
k
) be k elements of F
n
(
B
) considered asfreely chosen members. Let “P
k” be the corresponding vector.Any formulaF
(
P
k
,
Proj
) for which P
k are freely chosen members of F
n
(
B
) defines a subset of F
n
(
B
). According to the relation ≤, elements of this subset can be compared. In this specific case, the subset defined by F
(
P
k
,
Proj
) admits a minimal element and a maximal element.Theorem 15 (minimum and maximum of a Boolean formula).
Any formula
F
(
P
k, Proj) for which P
k are freely chosen members of F
n
(
B
) admits a minimum and a maximum defined as follows:
(52)
Min
⁡
P
k
∈
F
n
(
B
)
k
(
F
(
P
k
,
Proj
)
)
=
∏
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
)
Max
⁡
P
k
∈
F
n
(
B
)
k
(
F
(
P
k
,
Proj
)
)
=
∑
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
)
,Proof.
To prove this theorem, it is necessary to establish that(1)
∏
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
) is a lower bound of F
(
P
k
,
Proj
);
(2)
It exists at least one specific combination ofP
k for which F
(
P
k
,
Proj
)
=
∏
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
);
(3)
∑
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
) is an upper bound of F
(
P
k
,
Proj
);
(4)
It exists at least one specific combination ofP
k for which F
(
P
k
,
Proj
)
=
∑
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
).Details of this proof can be found in [24].


### 4.5.2. Optimization Problem

Considering the Boolean algebra ofn-variable switching functions (
F
n
(
B
)
,
+
,
·
,
-
,
0,1
),(i)
let(
f
Proj
1
,
…
,
f
Proj
n
) be the n
projection-functions of F
n
(
B
). Let “Proj” be the corresponding vector;
(ii)
Let(
x
1
,
…
,
x
k
) be k elements of F
n
(
B
) considered asunknowns. Let “X
k” be the corresponding vector;
(iii)
Let(
p
1
,
…
,
p
k
) be k elements of F
n
(
B
) considered asfreely chosen members. Let “P
k” be the corresponding vector.;
(iv)
LetEq
(
X
k
,
Proj
)
=
0 be the Boolean equation to solve;
(v)
LetF
C
(
X
k
,
Proj
) be the Boolean formula of the given criterion to optimize (maximization or minimization).The method we propose, to obtain the parametric form of thek-tuple of switching functions solution of Eq
(
X
k
,
Proj
)
=
0 according to a given optimization criterion F
C
(
X
k
,
Proj
) is composed of five steps as follows.(i)
The first step is to establish the parametric form of thek-tuple solution to Eq
(
X
k
,
Proj
)
=
0 only, thanks to Theorem 12.
(ii)
The second step is to establish the parametric form of the given optimization criterionF
C
(
X
k
,
Proj
) by substituting S
(
x
i
) for x
i. Let F
SC
(
P
k
,
Proj
) be the result of this substitution.
(iii)
The third step is to calculate the extremum ofF
SC
(
P
k
,
Proj
) according to Theorem 15. Let F
EC
(
Proj
) be the Boolean formula of this extremum.
(iv)
The fourth step is to replace the given criterion by the equivalent relation(53)
F
C
(
X
k
,
Proj
)
=
F
EC
(
Proj
)
.
(v)
The fifth step is to establish the parametric form of thek-tuple solution of the equivalent problem
(54)
Eq
(
X
k
,
Proj
)
=
0
F
Crit
(
X
k
,
Proj
)
=
F
ExtCrit
(
Proj
)
.


### 4.5.3. Partial Conclusions

Thanks to theorems presented in this section, it is now possible to obtain a parametric representation of the optimal solutions according to a given criterion, of any set of simultaneously asserted relations withk unknowns if a solution exists.The proposed method also permits to associate simultaneously or sequentially several criteria.(i)
When several criteria are treated simultaneously, the optimization problem can admit no solution. That is the case when the given criteria are antagonist.
(ii)
When several criteria are treated sequentially, the obtained solutions satisfy the criteria with a given priority order. An example of optimization with several criteria treated sequentially is presented in the next section.


## 4.5.1. Extrema of a Boolean Formula according to Freely Chosen Members ofF
n
(
B
)

Considering the Boolean algebra ofn-variable switching functions (
F
n
(
B
)
,
+
,
·
,
-
,
0,1
),(i)
let(
f
Proj
1
,
…
,
f
Proj
n
) be the n
projection-functions of F
n
(
B
);
(ii)
let(
p
1
,
…
,
p
k
) be k elements of F
n
(
B
) considered asfreely chosen members. Let “P
k” be the corresponding vector.Any formulaF
(
P
k
,
Proj
) for which P
k are freely chosen members of F
n
(
B
) defines a subset of F
n
(
B
). According to the relation ≤, elements of this subset can be compared. In this specific case, the subset defined by F
(
P
k
,
Proj
) admits a minimal element and a maximal element.Theorem 15 (minimum and maximum of a Boolean formula).
Any formula
F
(
P
k, Proj) for which P
k are freely chosen members of F
n
(
B
) admits a minimum and a maximum defined as follows:
(52)
Min
⁡
P
k
∈
F
n
(
B
)
k
(
F
(
P
k
,
Proj
)
)
=
∏
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
)
Max
⁡
P
k
∈
F
n
(
B
)
k
(
F
(
P
k
,
Proj
)
)
=
∑
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
)
,Proof.
To prove this theorem, it is necessary to establish that(1)
∏
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
) is a lower bound of F
(
P
k
,
Proj
);
(2)
It exists at least one specific combination ofP
k for which F
(
P
k
,
Proj
)
=
∏
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
);
(3)
∑
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
) is an upper bound of F
(
P
k
,
Proj
);
(4)
It exists at least one specific combination ofP
k for which F
(
P
k
,
Proj
)
=
∑
A
k
∈
{
0,1
}
k
‍
F
(
A
k
,
Proj
).Details of this proof can be found in [24].


## 4.5.2. Optimization Problem

Considering the Boolean algebra ofn-variable switching functions (
F
n
(
B
)
,
+
,
·
,
-
,
0,1
),(i)
let(
f
Proj
1
,
…
,
f
Proj
n
) be the n
projection-functions of F
n
(
B
). Let “Proj” be the corresponding vector;
(ii)
Let(
x
1
,
…
,
x
k
) be k elements of F
n
(
B
) considered asunknowns. Let “X
k” be the corresponding vector;
(iii)
Let(
p
1
,
…
,
p
k
) be k elements of F
n
(
B
) considered asfreely chosen members. Let “P
k” be the corresponding vector.;
(iv)
LetEq
(
X
k
,
Proj
)
=
0 be the Boolean equation to solve;
(v)
LetF
C
(
X
k
,
Proj
) be the Boolean formula of the given criterion to optimize (maximization or minimization).The method we propose, to obtain the parametric form of thek-tuple of switching functions solution of Eq
(
X
k
,
Proj
)
=
0 according to a given optimization criterion F
C
(
X
k
,
Proj
) is composed of five steps as follows.(i)
The first step is to establish the parametric form of thek-tuple solution to Eq
(
X
k
,
Proj
)
=
0 only, thanks to Theorem 12.
(ii)
The second step is to establish the parametric form of the given optimization criterionF
C
(
X
k
,
Proj
) by substituting S
(
x
i
) for x
i. Let F
SC
(
P
k
,
Proj
) be the result of this substitution.
(iii)
The third step is to calculate the extremum ofF
SC
(
P
k
,
Proj
) according to Theorem 15. Let F
EC
(
Proj
) be the Boolean formula of this extremum.
(iv)
The fourth step is to replace the given criterion by the equivalent relation(53)
F
C
(
X
k
,
Proj
)
=
F
EC
(
Proj
)
.
(v)
The fifth step is to establish the parametric form of thek-tuple solution of the equivalent problem
(54)
Eq
(
X
k
,
Proj
)
=
0
F
Crit
(
X
k
,
Proj
)
=
F
ExtCrit
(
Proj
)
.


## 4.5.3. Partial Conclusions

Thanks to theorems presented in this section, it is now possible to obtain a parametric representation of the optimal solutions according to a given criterion, of any set of simultaneously asserted relations withk unknowns if a solution exists.The proposed method also permits to associate simultaneously or sequentially several criteria.(i)
When several criteria are treated simultaneously, the optimization problem can admit no solution. That is the case when the given criteria are antagonist.
(ii)
When several criteria are treated sequentially, the obtained solutions satisfy the criteria with a given priority order. An example of optimization with several criteria treated sequentially is presented in the next section.


## 5. Algebraic Synthesis of Logical Controllers with Optimization Criteria and Incoherent Requirements

### 5.1. Control System Specifications

The studied system is the controller of a water supply system composed of two pumps which are working in redundancy (Figure4). The water distribution is made when it is necessary according to the possible failures of elements (the pumps and the distributing system).Figure 4
Structure of the water supply system.The expected behavior of the control system regarding the application requirements can be expressed by the set of assertions given hereafter:(i)
The two pumps never operate simultaneously.
(ii)
A pump cannot operate if it is out of order.
(iii)
When a global failure is detected, no pump can operate.
(iv)
Pumps can operate if and only if a water distribution request is present.
(v)
Priority is given according to “pr” (pump1 has priority when “pr” is true).
(vi)
In order to reduce the wear of the pumps, it is necessary to restrict the number of starting of the pumps.


#### 5.1.1. Inputs and Outputs of the Controller

The Boolean inputs and outputs of this controller are given in Figure5(a). Each pump is controlled thanks to a Boolean output (“p1” and “p2”). The controller is informed of water distribution requests thanks to the input “req.” Inputs “f1” and “f2” inform the controller of a failure of the corresponding pump and “gf” indicates a global failure of the installation. The values o or 1 of input “Pr” decide which pump has priority.Figure 5
Details of the case study.


#### 5.1.2. Control Laws to Synthetize

Our approach does not allow identifying automatically which state variables must be used. They are given by the designer according to its interpretation of the specification.For the water distribution system, we propose to use2 state variables, one for each output. According to this choice, 2
7-variable switching functions (P
1 and P
2) have to be synthesized (Figure 5(b)). They represent the unknowns of our problem. For this case study, the 7 projection-functions of F
7
(
B
) are therefore as follows.(i)
The5 switching functions (Rq, F
1, F
2, GF, and Pr) which characterize the behavior of the inputs of the controller and are defined as follows:
(55)
Rq:
B
7
⟶
B
(
rq
[
k
]
,
…
,
p
2
[
k
-
1
]
)
⟼
rq
[
k
]
.
(ii)
The2 switching functions (P
1
p and P
2
p) which characterize the previous behavior of the state variables of the controller and are defined as follows:
(56)
P

p
1:
B
7
⟶
B
(
rq
[
k
]
,
…
,
p
2
[
k
-
1
]
)
⟼
p
1
[
k
-
1
]
.


### 5.2. Algebraic Formalization of Requirements

The complete formalization of the behavior of the water distribution system is given in Figure5(c). In order to illustrate the power of expression of relations Equality and Inclusion, several examples (generic assertions and equivalent formal relations illustrated in the case study) are given hereafter. It is important to note that the relation Inclusion permits to express distinctly necessary conditions and sufficient conditions. This relation is the cornerstone of our approach.(i)
Pump1 and Pump2 never operate simultaneously:P
1
·
P
2
=
0;
(ii)
If Pump1 operates, Pump2 cannot operate:P
1
≤
P
2
¯;
(iii)
It is necessary to have a request for pumps operate:(
P
1
+
P
2
)
≤
Rq;
(iv)
It is sufficient to have a request for pumps operate:Rq
≤
(
P
1
+
P
2
);
(v)
When Pump1 is failed, it is sufficient to have a request for Pump2 operate:F
1
·
Rq
≤
P
2;
(vi)
When Pump1 is failed, it is necessary to have a request for Pump2 operate:F
1
·
P
2
≤
Rq.It is possible to prove that some of these formal expressions are equivalent (e.g., the first two). When a designer hesitates between two forms, he has the possibility, by using symbolic calculation, to check if the proposed relations are equivalent or not.AsP
1 and P
1
p represent the behavior of pump1 at, respectively, times [
k
] and [
k
-
1
], it is also possible to express relations about starts and stops of this pump as follows.(i)
It is necessary to have a request to start pump1:(
P
1
·
P
1
p
¯
)
≤
Rq.
(ii)
When pump1 operates, it is sufficient to have a global failure to stop pump1:(
P
1
p
·
GF
)
≤
(
P
1
¯
·
P
1
p
).


### 5.3. Synthesis Process

In traditional design methods, the design procedure of a logic controller is not a linear process, but an iterative one converging to an acceptable solution. At the beginning of the design, requirements are neither complete nor without errors. Most often, new requirements are added during the search of solutions, and others are corrected. This complementary information is given by the designer after analysis of the partial solutions he found or when inconsistencies have been detected. If we do not make the hypothesis that the specifications are complete and consistent, designing a controller with a synthesis technique is also an iterative process in which the designer plays an important role.


#### 5.3.1. Analysis of Requirements

For this case study, we choose to start with requirements R1 to R6. For this subset of requirements, the result given by your software tool was the following inconsistency condition:I
=
Rq
·
GF
+
Rq
·
F
1
·
F
2.Since requirements are declared inconsistent, we have to give complementary information to precise our specification. By analyzing each term of this formula, it is possible to detect the origin of the inconsistency:(i)
Rq
·
GF: what happens if we have simultaneously a request and a global failure? We consider that requirement R4 is more important than requirement R6 (R4 ≫ R6) as no pump can operate for this configuration.
(ii)
Rq
·
F
1
·
F
2: what happens if we have simultaneously a request and a failure of each pump? We consider that requirements R2 and R3 are more important than requirement R6 (
{
R
2
,
R
3
}
≫
R
6
).With these priority rules, all the requirements are now coherent and the set of all the solutions can be computed.


#### 5.3.2. Optimal Solutions

For choosing a control law of the water supply system among this set of possible solutions, we will now take into account the given optimization criteria. The first criterion aims at minimizing the number of starting of each pump in order to reduce its wear. The second criterion aims at maximizing the use of the pump indicated by the value of parameterPr. The method we propose allows proving that proposed criteria cannot be treated simultaneously since they are antagonist (to strictly the priority use of the pump fixed by parameter Pr, it is necessary to permute pumps when Pr changes of value, implying a supplementary start of a pump). Details can be found in [25].All the priorities rules and optimization criteria used for this case study are given in Figure5(c). The solution we obtain is proposed in Figure 5(d).


#### 5.3.3. Implementing Control Laws

The synthesized control laws presented in Figure5(e) have been obtained by translating the expression of the two unknowns according to the projection-functions into relations between recurrent Boolean equations. These control laws can be automatically translated in the syntax of the ladder diagram language [1] before being implemented into a PLC. The code is composed of only 4 rungs (Figure 6).Figure 6
Ladder diagram of the code to implement into the PLC.The synthesized control laws can be given under the form of an automatically built input/output automaton with guarded transitions [21] (Figure 7).Figure 7
State model of the obtained control law.


## 5.1. Control System Specifications

The studied system is the controller of a water supply system composed of two pumps which are working in redundancy (Figure4). The water distribution is made when it is necessary according to the possible failures of elements (the pumps and the distributing system).Figure 4
Structure of the water supply system.The expected behavior of the control system regarding the application requirements can be expressed by the set of assertions given hereafter:(i)
The two pumps never operate simultaneously.
(ii)
A pump cannot operate if it is out of order.
(iii)
When a global failure is detected, no pump can operate.
(iv)
Pumps can operate if and only if a water distribution request is present.
(v)
Priority is given according to “pr” (pump1 has priority when “pr” is true).
(vi)
In order to reduce the wear of the pumps, it is necessary to restrict the number of starting of the pumps.


### 5.1.1. Inputs and Outputs of the Controller

The Boolean inputs and outputs of this controller are given in Figure5(a). Each pump is controlled thanks to a Boolean output (“p1” and “p2”). The controller is informed of water distribution requests thanks to the input “req.” Inputs “f1” and “f2” inform the controller of a failure of the corresponding pump and “gf” indicates a global failure of the installation. The values o or 1 of input “Pr” decide which pump has priority.Figure 5
Details of the case study.


### 5.1.2. Control Laws to Synthetize

Our approach does not allow identifying automatically which state variables must be used. They are given by the designer according to its interpretation of the specification.For the water distribution system, we propose to use2 state variables, one for each output. According to this choice, 2
7-variable switching functions (P
1 and P
2) have to be synthesized (Figure 5(b)). They represent the unknowns of our problem. For this case study, the 7 projection-functions of F
7
(
B
) are therefore as follows.(i)
The5 switching functions (Rq, F
1, F
2, GF, and Pr) which characterize the behavior of the inputs of the controller and are defined as follows:
(55)
Rq:
B
7
⟶
B
(
rq
[
k
]
,
…
,
p
2
[
k
-
1
]
)
⟼
rq
[
k
]
.
(ii)
The2 switching functions (P
1
p and P
2
p) which characterize the previous behavior of the state variables of the controller and are defined as follows:
(56)
P

p
1:
B
7
⟶
B
(
rq
[
k
]
,
…
,
p
2
[
k
-
1
]
)
⟼
p
1
[
k
-
1
]
.


## 5.1.1. Inputs and Outputs of the Controller

The Boolean inputs and outputs of this controller are given in Figure5(a). Each pump is controlled thanks to a Boolean output (“p1” and “p2”). The controller is informed of water distribution requests thanks to the input “req.” Inputs “f1” and “f2” inform the controller of a failure of the corresponding pump and “gf” indicates a global failure of the installation. The values o or 1 of input “Pr” decide which pump has priority.Figure 5
Details of the case study.


## 5.1.2. Control Laws to Synthetize

Our approach does not allow identifying automatically which state variables must be used. They are given by the designer according to its interpretation of the specification.For the water distribution system, we propose to use2 state variables, one for each output. According to this choice, 2
7-variable switching functions (P
1 and P
2) have to be synthesized (Figure 5(b)). They represent the unknowns of our problem. For this case study, the 7 projection-functions of F
7
(
B
) are therefore as follows.(i)
The5 switching functions (Rq, F
1, F
2, GF, and Pr) which characterize the behavior of the inputs of the controller and are defined as follows:
(55)
Rq:
B
7
⟶
B
(
rq
[
k
]
,
…
,
p
2
[
k
-
1
]
)
⟼
rq
[
k
]
.
(ii)
The2 switching functions (P
1
p and P
2
p) which characterize the previous behavior of the state variables of the controller and are defined as follows:
(56)
P

p
1:
B
7
⟶
B
(
rq
[
k
]
,
…
,
p
2
[
k
-
1
]
)
⟼
p
1
[
k
-
1
]
.


## 5.2. Algebraic Formalization of Requirements

The complete formalization of the behavior of the water distribution system is given in Figure5(c). In order to illustrate the power of expression of relations Equality and Inclusion, several examples (generic assertions and equivalent formal relations illustrated in the case study) are given hereafter. It is important to note that the relation Inclusion permits to express distinctly necessary conditions and sufficient conditions. This relation is the cornerstone of our approach.(i)
Pump1 and Pump2 never operate simultaneously:P
1
·
P
2
=
0;
(ii)
If Pump1 operates, Pump2 cannot operate:P
1
≤
P
2
¯;
(iii)
It is necessary to have a request for pumps operate:(
P
1
+
P
2
)
≤
Rq;
(iv)
It is sufficient to have a request for pumps operate:Rq
≤
(
P
1
+
P
2
);
(v)
When Pump1 is failed, it is sufficient to have a request for Pump2 operate:F
1
·
Rq
≤
P
2;
(vi)
When Pump1 is failed, it is necessary to have a request for Pump2 operate:F
1
·
P
2
≤
Rq.It is possible to prove that some of these formal expressions are equivalent (e.g., the first two). When a designer hesitates between two forms, he has the possibility, by using symbolic calculation, to check if the proposed relations are equivalent or not.AsP
1 and P
1
p represent the behavior of pump1 at, respectively, times [
k
] and [
k
-
1
], it is also possible to express relations about starts and stops of this pump as follows.(i)
It is necessary to have a request to start pump1:(
P
1
·
P
1
p
¯
)
≤
Rq.
(ii)
When pump1 operates, it is sufficient to have a global failure to stop pump1:(
P
1
p
·
GF
)
≤
(
P
1
¯
·
P
1
p
).


## 5.3. Synthesis Process

In traditional design methods, the design procedure of a logic controller is not a linear process, but an iterative one converging to an acceptable solution. At the beginning of the design, requirements are neither complete nor without errors. Most often, new requirements are added during the search of solutions, and others are corrected. This complementary information is given by the designer after analysis of the partial solutions he found or when inconsistencies have been detected. If we do not make the hypothesis that the specifications are complete and consistent, designing a controller with a synthesis technique is also an iterative process in which the designer plays an important role.


### 5.3.1. Analysis of Requirements

For this case study, we choose to start with requirements R1 to R6. For this subset of requirements, the result given by your software tool was the following inconsistency condition:I
=
Rq
·
GF
+
Rq
·
F
1
·
F
2.Since requirements are declared inconsistent, we have to give complementary information to precise our specification. By analyzing each term of this formula, it is possible to detect the origin of the inconsistency:(i)
Rq
·
GF: what happens if we have simultaneously a request and a global failure? We consider that requirement R4 is more important than requirement R6 (R4 ≫ R6) as no pump can operate for this configuration.
(ii)
Rq
·
F
1
·
F
2: what happens if we have simultaneously a request and a failure of each pump? We consider that requirements R2 and R3 are more important than requirement R6 (
{
R
2
,
R
3
}
≫
R
6
).With these priority rules, all the requirements are now coherent and the set of all the solutions can be computed.


### 5.3.2. Optimal Solutions

For choosing a control law of the water supply system among this set of possible solutions, we will now take into account the given optimization criteria. The first criterion aims at minimizing the number of starting of each pump in order to reduce its wear. The second criterion aims at maximizing the use of the pump indicated by the value of parameterPr. The method we propose allows proving that proposed criteria cannot be treated simultaneously since they are antagonist (to strictly the priority use of the pump fixed by parameter Pr, it is necessary to permute pumps when Pr changes of value, implying a supplementary start of a pump). Details can be found in [25].All the priorities rules and optimization criteria used for this case study are given in Figure5(c). The solution we obtain is proposed in Figure 5(d).


### 5.3.3. Implementing Control Laws

The synthesized control laws presented in Figure5(e) have been obtained by translating the expression of the two unknowns according to the projection-functions into relations between recurrent Boolean equations. These control laws can be automatically translated in the syntax of the ladder diagram language [1] before being implemented into a PLC. The code is composed of only 4 rungs (Figure 6).Figure 6
Ladder diagram of the code to implement into the PLC.The synthesized control laws can be given under the form of an automatically built input/output automaton with guarded transitions [21] (Figure 7).Figure 7
State model of the obtained control law.


## 5.3.1. Analysis of Requirements

For this case study, we choose to start with requirements R1 to R6. For this subset of requirements, the result given by your software tool was the following inconsistency condition:I
=
Rq
·
GF
+
Rq
·
F
1
·
F
2.Since requirements are declared inconsistent, we have to give complementary information to precise our specification. By analyzing each term of this formula, it is possible to detect the origin of the inconsistency:(i)
Rq
·
GF: what happens if we have simultaneously a request and a global failure? We consider that requirement R4 is more important than requirement R6 (R4 ≫ R6) as no pump can operate for this configuration.
(ii)
Rq
·
F
1
·
F
2: what happens if we have simultaneously a request and a failure of each pump? We consider that requirements R2 and R3 are more important than requirement R6 (
{
R
2
,
R
3
}
≫
R
6
).With these priority rules, all the requirements are now coherent and the set of all the solutions can be computed.


## 5.3.2. Optimal Solutions

For choosing a control law of the water supply system among this set of possible solutions, we will now take into account the given optimization criteria. The first criterion aims at minimizing the number of starting of each pump in order to reduce its wear. The second criterion aims at maximizing the use of the pump indicated by the value of parameterPr. The method we propose allows proving that proposed criteria cannot be treated simultaneously since they are antagonist (to strictly the priority use of the pump fixed by parameter Pr, it is necessary to permute pumps when Pr changes of value, implying a supplementary start of a pump). Details can be found in [25].All the priorities rules and optimization criteria used for this case study are given in Figure5(c). The solution we obtain is proposed in Figure 5(d).


## 5.3.3. Implementing Control Laws

The synthesized control laws presented in Figure5(e) have been obtained by translating the expression of the two unknowns according to the projection-functions into relations between recurrent Boolean equations. These control laws can be automatically translated in the syntax of the ladder diagram language [1] before being implemented into a PLC. The code is composed of only 4 rungs (Figure 6).Figure 6
Ladder diagram of the code to implement into the PLC.The synthesized control laws can be given under the form of an automatically built input/output automaton with guarded transitions [21] (Figure 7).Figure 7
State model of the obtained control law.


## 6. Discussion

In our approach, the synthesis of control laws is based on the symbolic calculation, a prototype software tool has been developed to avoid tedious calculus and to aid the designer during the different steps of the synthesis. This tool (that can be obtained on request by the authors) performs all the computations required for inconsistencies detection between requirements and for control laws generation. In this tool, all the Boolean formulas are stored in the form of reduced ordered binary decision diagrams, which allows efficient calculations. For example, the computations for synthesizing a controller for the water supply system that we developed above have been made in less than 10 ms onto a classical laptop.Our approach has been tested on several studies cases (some of them are available online:http://www.lurpa.ens-cachan.fr/-226050.kjsp). The feedbacks of these experiences allowed us to identify some of its limits and its possibilities; the most important are given below.We have first to recall that our method can only be used for binary systems (systems whose inputs and outputs of their controller are Boolean values). Nevertheless, in practice many systems, like manufacturing systems, transport systems, and so on, are fully or partially binary.In our opinion the main advantage of our approach is that, contrary to traditional engineering approaches, the synthesized control laws are not depending on designer’s skill or of his correct interpretation of the system requirements. On the other hand, the quality of the synthesis results highly depends on the relevance of the requirements proposed by the designer. This step of formalization, by the designer, of the informal requirements of the system to be controlled is the Achilles heel of all synthesis methods, including the Supervisory Control Theory (SCT), and cannot be automated.The objective comparison of our approach with other synthesis methods, and more especially with SCT, is very difficult because the models used and the theoretical basics are very different. Nevertheless, we tested both approaches on same study cases. One of them, the control of an automatic parking gate, has been published in [26]. The results obtained in this case are summarized in Table 1.Table 1
Futures concerning a same case study.
Formal requirements
Synthesized controller
PLC program (structured text)
Supervisory Control Theory
Plant behavior: 11 finite automata(481 states and 1330 transitions) Specifications: 11 finite automata
Finite automaton of 45 states and 70 transitions
130 lines
Algebraic synthesis
8 equations and 2 priority rules
2 6-variable switching functions
4 linesFurthermore, one may note that the supervisor that is synthesized by SCT is optimal in the sense where it is the most permissive; that is, the one that reduces the less the plant behavior in order to force it to respect the specifications. As shown in this paper our method allows to cope with inconsistencies in specifications, what is not possible with SCT, and also allows to find optimal controllers by choosing different optimization criteria (most permissive, most restrictive, most safe controller, etc.).


## 7. Conclusion

Many research works in the field of DES aim at formalizing steps of the systems life cycle. Since 20 years, significant progresses have been obtained for the synthesis, verification, performance evaluation, and diagnosis of DESs. Nevertheless, one of the common difficulties of these works is the translation of informal expression of the knowledge of a system into formal requirements. Few works have paid attention to this important task which is very error prone. In this paper, we proposed an iterative process that allows coping with inconsistencies of the requirements during the synthesis of the controller. The framework in which we proposed this approach is an algebraic synthesis method. Since the problem is located in the frontier between formal and informal, intervention of the designer is necessary. Nevertheless, we have shown that this intervention can be guided by the results of the formal method provides.



---

*Source: 726246-2014-05-28.xml*