Komposition von Bedingung-/Ereignissystemen und deren Echtzeitvarianten

Diplomarbeit

vorgelegt von Ben Lukoschus im August 1998

Betreuung: Prof. Dr. Willem-Paul de Roever Dr. rer. nat. Yassine Lakhnech

Christian-Albrechts-Universität zu Kiel Institut für Informatik und Praktische Mathematik

2

Contents

1 Introduction 7

2 Condition/Event Systems 15 2.1 Basic Notions . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.2 Condition/Event Systems . . . . . . . . . . . . . . . . . . . . 17 2.3 Discrete Condition/Event Systems . . . . . . . . . . . . . . . 18

3 Connecting Condition/Event Systems 23

3.1 The Cascade Interconnection . . . . . . . . . . . . . . . . . . . 24 3.1.1 The Cascade Interconnection of C/E Systems . . . . . 24 3.1.2 The Cascade Interconnection of Discrete C/E Systems 25

3.2 The Feedback Connection . . . . . . . . . . . . . . . . . . . . 28 3.2.1 The Feedback Connection of C/E Systems . . . . . . . 28 3.2.2 The Feedback Connection of Discrete C/E Systems . . 29

3.3 The Loop Interconnection . . . . . . . . . . . . . . . . . . . . 33 3.3.1 The Loop Interconnection of C/E Systems . . . . . . . 34 3.3.2 The Loop Interconnection of Discrete C/E Systems . . 35 3.3.3 Properties of the Discrete Loop Interconnection …. 39 3.3.4 Special Cases of the Discrete Loop Interconnection . . 41

4 The Parallel Interconnection 47

4.1 Adding Component Names to C/E Systems . . . . . . . . . . 48 4.1.1 Named C/E Systems . . . . . . . . . . . . . . . . . . . 49 4.1.2 Named Discrete C/E Systems . . . . . . . . . . . . . . 50

4.2 The Parallel Interconnection of C/E Systems . . . . . . . . . . 51 4.3 The Parallel Interconnection of Discrete C/E Systems . . . . . 54 4.4 Hiding Output Components in CESs and DCESs . . . . . . . 59 4.5 Special Cases of the Discrete Parallel Interconnection . . . . . 63 4.6 Weakening the Unique Solution Property . . . . . . . . . . . . 67 5 Introducing Quantitative Timing 79

5.1 Timers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 5.2 Timed Condition/Event Systems . . . . . . . . . . . . . . . . 82 5.3 The Parallel Interconnection of Timed C/E Systems . . . . . . 86

6 Example: The Evaporator System 91 6.1 The Problem . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 6.2 The Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93

6.2.1 The Modules . . . . . . . . . . . . . . . . . . . . . . . 95 6.3 Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104

6.3.1 Using Timing Diagrams . . . . . . . . . . . . . . . . . 105 6.3.2 Using Timed Automata . . . . . . . . . . . . . . . . . 107 6.3.3 Using the Parallel Interconnection Operator . . . . . . 108

7 Conclusion 113

Bibliography 115

List of Figures

1.1 Example of an algebraic loop . . . . . . . . . . . . . . . . . . 9

2.1 Example of a condition signal . . . . . . . . . . . . . . . . . . 16 2.2 Example of an event signal . . . . . . . . . . . . . . . . . . . . 17 2.3 A block diagram of a condition/event system . . . . . . . . . . 18

3.1 CES cascade interconnection of S_{1} and S_{2} . . . . . . . . . . . 24 3.2 The feedback connection in [SK91] . . . . . . . . . . . . . . . 28 3.3 CES feedback connection of S . . . . . . . . . . . . . . . . . . 29 3.4 CES loop interconnection of S_{1} and S_{2} . . . . . . . . . . . . . 34 3.5 Modeling feedback of D by loop using the system D_{id} . . . . . 44

4.1 Example of a parallel interconnection . . . . . . . . . . . . . . 52 4.2 The composition of the system in Figure 4.1 . . . . . . . . . . 52 4.3 Mutually connected DCESs . . . . . . . . . . . . . . . . . . . 55 4.4 Modeling feedback by parallel using D_{id} . . . . . . . . . . . . . 67 4.5 A system with two solutions for the feedback value . . . . . . 68 4.6 A parallel interconnection of DCESs with multiple solutions . 76 4.7 Block diagram of D = D_{1} ||| D_{2} . . . . . . . . . . . . . . . . . 77

5.1 Example of a timer function . . . . . . . . . . . . . . . . . . . 80 5.2 Block diagram of a timed condition/event system . . . . . . . 83

6.1 Diagram of the evaporator system . . . . . . . . . . . . . . . . 92 6.2 Block diagram of the evaporator system model . . . . . . . . . 94 6.3 Block diagram of the TCES Tank-1 . . . . . . . . . . . . . . . 96 6.4 Discrete part of the TCES Tank-1 . . . . . . . . . . . . . . . 96 6.5 Block diagram of the TCES Tank-2 . . . . . . . . . . . . . . . 98 6.6 Discrete part of the TCES Tank-2 . . . . . . . . . . . . . . . 99 6.7 Block diagram of the TCES Heater . . . . . . . . . . . . . . . 99 6.8 Discrete part of the TCES Heater . . . . . . . . . . . . . . . . 100 6.9 Block diagram of the DCES Condenser . . . . . . . . . . . . . 100 6.10 Discrete part of the DCES Condenser . . . . . . . . . . . . . . 100 6.11 Block diagram of the TCES Pressure . . . . . . . . . . . . . . 101 6.12 Discrete part of the TCES Pressure . . . . . . . . . . . . . . . 101 6.13 Block diagram of the TCES Controller . . . . . . . . . . . . . 102 6.14 Discrete part of the TCES Controller . . . . . . . . . . . . . . 103 6.15 A timing diagram for the evaporator system . . . . . . . . . . 106 6.16 Block diagram of the TCES PressCond . . . . . . . . . . . . . 110 6.17 Discrete part of the TCES PressCond . . . . . . . . . . . . . . 111 6.18 The reachable discrete part of the TCES PressCond . . . . . . 111

Chapter 1

Introduction

When building a computer controlled system, one has to ensure that it works properly, that is, according to its specifications. Often it is considered that “good faith” in programmers, system builders, and advanced technology is enough to create error free systems. And often enough, this short-minded (or short-financed) attitude causes loss of money, time, or even lives, e.g., [Lev95].

In the design of critical systems such as nuclear power plants, planes, medical devices, or small robots moving on the surface of Mars, more than just “good faith” is needed to ensure compliance with the specifications. The first step into that direction is a formal framework where the system design and the system requirements can be embedded.

In this formal framework, large systems should be dividable into smaller ones, called modules, which are connected in some way to exchange information. This is called modularity. Among the advantages of modularity are the reusability of modules, the ability to split up work during system design, and compositional reasoning [HdR86, HdR90] in verification, model checking, and testing. A common method for representing modular structures in system engineering and control theory is the use of block diagrams and signal flows.

The framework used in this thesis is the model of condition/event systems (CESs), which are introduced in [SK91]. CESs are a class of continuous-time discrete event systems and can be represented graphically as block diagrams. Communication between CESs takes place by exchanging two different kinds of symbols, called condition and event symbols. A set of condition or event symbols is called condition or event alphabet. Condition symbols are used to describe system states and to enable or disable state changes, whereas event symbols denote certain actions at discrete points in time and can be used to trigger state changes. To describe the semantics of a CES, condition and event signals are used. A signal is a function which maps points in time to a condition or event alphabet, i.e., at each moment, one symbol of an alphabet is visible. The behavior of a CES is given by a function which associates with each pair of an input condition signal and an input event signal a nonempty set of possible outputs, which are pairs of output condition signals and output event signals.

This way of describing a system’s behavior has some disadvantages. The behavior of a CES is given by relating signals, and one signal describes the current symbol visible at a CES’s input or output component for all points in time. This is a very abstract view, since normally a dynamic system’s output symbols at a certain moment depend only on its internal state and its input symbols at that very moment. Furthermore, we would like to have an operational description of the system using functions mapping input symbols to output symbols (and not relating signals like in CESs), since this makes the implementation and the reasoning about systems much easier. Therefore, we introduce discrete condition/event systems (DCESs), which communicate using the same symbols as CESs, but are described operationally using a finite set of internal states, a transition function, and output functions which compute output symbols using the current internal state and the current input symbols. So a DCES can be understood as a finite automaton having two output functions, one for conditions and one for events. The semantics of a DCES is described as a CES, but not every behavior of a CES is expressible using a DCES.

In the step from CESs to DCESs, however, we lose quantitative timing, i.e., in the DCES model, we have no means of measuring time. Since many critical systems are based on strong timing requirements, we introduce timers. A timer has an internal clock which increases linearly with the global time and can be reset by an external event. Semantically, timers are modeled as a class of CESs. Using these timers, timed condition/event systems (TCESs) are defined in [Kow95] in the spirit of timed automata [AD94]. A TCES is simply a DCES which is connected to a set of timers. With each timer we associate a list of thresholds, which are integers the timer value can be compared to. In addition to the reset event signal received from the DCES, each timer has a condition signal denoting in which interval between the thresholds the current timer value is. Furthermore, timers use an event signal to notify the DCES whenever the timer value equals exactly one of the thresholds.

For compositional reasoning about condition/event systems, the notions of cascade and feedback connections to compose CESs and DCESs are presented in [SK91]. These connections are very restrictive in the sense that they do not provide many ways of connecting systems, e.g., feedback allows no additional external input signals. Moreover, there is no formal framework for composing TCESs.

In this thesis we present a formal framework for composing DCESs and TCESs. Intuitively, systems are composed by connecting output components to input components, and the signals of the connected components have to be equal. We discuss the following two questions which arise when constructing a system consisting of some interconnected modules (DCESs in our framework):

1. Can we express the semantics of the system by using the semantics of its modules?

2. Can we compose the modules into one DCES having the same semantics as the compound system?

For answering these questions, we must of course have a formal definition of the semantics of the compound system. This must not necessarily be expressible in the way we express the semantics of the parts.

The answers to both questions depend on the way the systems are connected. If there are no interconnections at all, i.e., the parts do not exchange any information and are independent from each other, both answers are obviously yes. We simply can use Cartesian products of the parts’ signals to form the signals of the compound system (this answers question 1), and we can use a Cartesian product of the parts’ sets of states to gain the set of states for the DCES needed in question 2. No synchronization is needed, since the parts have no common signals.

If there are interconnections of the parts, which is usually the case for nontrivial systems, the answers are not that easy to find. Although question 1 might be positively answered, a DCES for question 2 may not exist due to so-called algebraic loops. For example, consider the two DCESs D_{1} and D_{2} in Figure 1.1. Both systems are mutually connected by condition signals that can take the values “a” or “b”. D_{1} just copies its input (from D_{2}) to its output (to D_{2}), while D_{2} is an inverter, i.e., input “a” yields output “b” and input “b” yields output “a”. Since we have no time delays during communication in

D_{1}^{a ↦ a}^{b ↦ b}  ^{\overline{}} D_{2}^{a ↦ b}^{b ↦ a}^{\overline{}}

Figure 1.1: Example of an algebraic loop our model, this connection leads to contradiction; there are no feasible values for the symbols exchanged between D_{1} and D_{2}, and therefore, no DCES for the composed system can be given.

In synchronous languages, much research is done to examine such algebraic loops. One way of dealing with this is to demand unique solutions for the symbols between D_{1} and D_{2} (e.g. in [CPHP87, BG92, Hal93]). Systems which do not fulfill this property must not have that kind of mutual connection. Another way is to demand that there exists at least one solution (e.g. in [BG90, GGB87, Hal93]).

If the answer to question 2 is yes, one is interested in a composition operator which effectively constructs the DCES for the compound system, using the parts and information about the connections between them. For different kinds of interconnections, different composition operators have to be defined. In [SK91] two operators are given: The cascade interconnection operator defines the connection of a DCES’s outputs with the inputs of another DCES, and the feedback connection operator defines the connection of a DCES’s outputs with its own inputs. We additionally define the loop interconnection operator (where two DCESs are mutually connected like in Figure 1.1) and the parallel interconnection operator, which allows arbitrary connections among a set of DCESs. Two versions of the parallel interconnection operator are defined, one to handle systems with unique solutions and one for the case with multiple solutions. Both the loop and the parallel operator are also able to express feedback and cascade.

For verifying and model checking modularly composed systems, one can use the composition operators to combine all parts into one single system which then can be checked with respect to the desired properties. Such approaches often break space and time limits due to the state explosion problem. A more promising way is to find out which parts of the system are really needed to check a certain property; only these parts are then composed and checked.

In [Huu98], TCESs are transformed into timed automata, which then can be model checked with tools like KRONOS [OY93], UPPAAL [BLL^{+}96], or HyTech [HHWT95, HH95]. This provides a wide range of possibilities to examine properties of TCESs by using existing tools for timed automata instead of building a new model checker.

Structure of this Work

The main goal of this thesis is to provide useful operators for composing discrete condition/event systems as well as timed condition/event systems. We take a look at the existing operators of [SK91] (cascade interconnection and feedback connection) and reason about their applicability to large interconnected systems. We believe that these operators are not flexible enough to allow easy handling of complex interconnections. Therefore, we define the parallel interconnection operator which allows us to compose any finite number of systems with any kind of interconnection structure, provided a certain property forbidding algebraic loops holds.

We start in Chapter 2 with the basic notions like condition symbols, event symbols, and signals. Condition/event systems are defined as systems which relate input and output signals. Then we introduce discrete condition/event systems syntactically as finite transition systems with output functions for conditions and events. The semantics of a DCES is defined as a CES by using the notion of a run of the DCES over input and output signals, that is, a function mapping time to discrete states of the DCES such that the transition function and the output functions behave in accordance to the given signals.

Chapter 3 introduces the cascade interconnection, which is first defined for CESs in a descriptive way, that is, a CES S is said to be a cascade interconnection of two given CESs S_{1} and S_{2}, if certain conditions hold. The nature of such a descriptive definition is that such a system S must not exist for all S_{1} and S_{2}. In the discrete case however, we prove that for all DCESs D_{1} and D_{2} where D_{1}’s output alphabets match D_{2}’s input alphabets, a DCES D can be effectively constructed such that the semantics of D is a cascade interconnection of the semantics of D_{1} and D_{2}. This effective construction defines the cascade interconnection operator for DCESs.

Then the feedback connection is defined, first in a descriptive way for CESs. We show that a feedback connection does not exist for all CESs. In the discrete case, we prove that for all DCESs D where the output alphabets match the input alphabets, a DCES D′ can be effectively constructed such that the semantics of D′ is a feedback connection of the semantics of D, if a unique solution property is satisfied. This property is used to avoid algebraic loops in the feedback signals. The feedback connection operator for DCESs is defined by this effective construction.

We conclude Chapter 3 by defining the loop interconnection for CESs and the loop interconnection operator for DCESs. This describes a mutual connection between systems like in Figure 1.1. Again, a unique solution property is used in the discrete case to avoid algebraic loops. We show that the loop operator is able to express cascade as well as feedback.

In Chapter 4, we present an even more flexible way of connecting systems, the parallel interconnection. It allows arbitrary connections between systems, whereas all operators defined before have strong restrictions on the way systems can be connected. We obtain this new flexibility by introducing names to identify system components, and then consider components of different systems to be connected if they have the same name. Therefore, named CESs and named DCESs are introduced and used instead of CESs and DCESs. Our first version of the parallel interconnection operator again uses a unique solution property and is able to express cascade, feedback, and loop. After defining a hiding operator which removes output signals from CESs and DCESs, we present a second version of the parallel interconnection operator, which is able to handle multiple solutions for the signals connecting the subsystems.

Quantitative timing is considered in Chapter 5. We introduce timed condition/event systems as an extension of DCESs with features for quantitative timing. This is done by introducing timers, which are CESs that operate like a clock and can be reset by an external input event. The outputs of a timer are condition and event signals denoting where between a list of threshold values the current timer value is. A TCES is defined as a DCES which is connected to a set of timers. The DCES can reset timers via reset events and is able to use the information about the timer values to integrate quantitative timing into its transition and output functions.

Our multiple solution version of the parallel interconnection operator is augmented to systems consisting of TCESs instead of DCESs. Also the unique solution version can be expressed for TCESs. With these operators, we have reached our goal to present a powerful set of operators for composing timed condition/event systems.

An extensive example for the composition of TCESs is given in Chapter 6, where a part of a chemical laboratory batch plant is presented and modeled as a parallel interconnection of TCESs.

The last chapter contains conclusions and points out further work.

Acknowledgments

Parts of this work have been supported by the German Research Council (Deutsche Forschungsgemeinschaft DFG) within the special program KON-DISK (Analysis and Synthesis of Technical Systems with Continuous-discrete Dynamics) under the grants Ro 1122/2 and En 152/19.

Willem-Paul de Roever and his research assistants, especially Yassine Lakhnech, have shown high motivation to introduce me to the world of scientific research. They tried to show me as many aspects as possible—and they succeeded! I thank them for many memorable events, like the visit to Grenoble and the workshops at Malente.

It has always been a pleasure to work with my fellow students; I especially thank Ralf Huuck and Karsten Stahl for proof reading and many corrections under my severe “last minute” conditions.

Finally, special thanks to my parents, who have been supportive at all times in many different ways.

Notations

We present notational conventions used throughout this work. For a set X, we denote by 2^{X} the set of all subsets of X. Given a finite set D and a function r : ℝ_{≥0} → D, we call r finite-variable, if in any bounded subinterval of ℝ_{≥0}, r changes its value only finitely often, i.e, r has only a finite number of discontinuity points. If r is finite-variable, r is furthermore called rightcontinuous, if for all t ∈ ℝ_{≥0} there exists an ε > 0 such that r(t + x) = r(t) for all x ∈ (0, ε). And for any finite-variable r, we define for all t ∈ ℝ_{>0} the limit from the left of r at t: r(t^{−}) = lim_{ε→0}^{ε>0} r(t − ε).

For any n-tuple x, we denote by x_{i} the projection of x on its ith component. This notion is extended to Cartesian products of sets and to functions having a Cartesian product as range. The domain of a function f is denoted by dom(f), and its range by ran(f).

14

Condition/Event Systems

Condition/event systems (CESs) are a class of continuous-time discrete event systems and have been introduced in [SK91]. The CES model is widely used to describe the behavior of discrete and hybrid systems. It allows to develop complex systems by means of block diagrams and signal flows, which is standard practice in system theory. A CES is defined as a relation between input and output signals. A signal can be understood as a function mapping points in time to a finite set, called alphabet, of symbols representing time-dependent information. A signal uses one of two different kinds of symbols, namely condition symbols and event symbols. Condition signals are piecewise constant functions and are used to represent time-dependent system states by condition symbols like “on”, “off”, or “waiting”. Conditions symbols can be used to enable or disable transitions in systems with discrete state realizations. Event signals map points in time to a special null symbol except for some discrete points, in which so-called proper events occur. Proper events represent instantaneous actions like “start”, “stop”, or “reset”; they can be used to force transitions in a discrete state system in such a way that a transition is taken exactly at the moment the event occurs.

In this chapter, we formally define condition/event systems. We also introduce a model of condition/event systems with discrete state realizations, called discrete condition/event systems.

2.1 Basic Notions

Let D be a set of symbols. These will be the symbols in the range of condition and event signals.

Definition 2.1 (Condition alphabet, event alphabet) A condition alphabet is a nonempty, finite set U ⊆ D, and its elements are called condition symbols or simply conditions.^{1}

An event alphabet is a nonempty, finite set V ⊆ D containing a special null symbol 0_{V}. Any v ∈ V is called event symbol, or simply event, and if v ≠ 0_{V}, it is also called proper event. □

We write 0 for the null symbol 0_{V}, if the event alphabet V is known from the context. A Cartesian product V = V_{1} × … × V_{n} of event alphabets is also an event alphabet, and we abbreviate its null symbol (0_{V_{1}}, …, 0_{V_{n}}) also with 0_{V} or 0. In the following, we will use the letters U and Y for condition alphabets, and V and Z for event alphabets.

Condition and event alphabets serve as the range for condition signals and event signals, which are functions mapping points in time to such alphabets. In our framework, time is modeled by the set ℝ_{≥0} of nonnegative real numbers.

[figure: t; s_{U}(t); off; on; auto; 0]

Figure 2.1: Example of a condition signal

Definition 2.2 (Condition signal, event signal) A condition signal over a condition alphabet U is a right-continuous, finite-variable function s_{U} : ℝ_{≥0} → U. The set of all condition signals over U is denoted by C(U).

An event signal over an event alphabet V is a function s_{V} : ℝ_{≥0} → V, if s_{V} (0) = 0 and for any bounded subinterval I of ℝ_{≥0}, there are only finitely many t ∈ I with s_{V} (t) ≠ 0. The set of all event signals over V is denoted by E(V). □

1The reader is warned not to confuse the usage of “condition” as an abbreviation for “condition symbol” with the notion of “condition” for “property”, “prerequisite”, “Boolean guard”, etc.

Figure 2.1 shows an example of a condition signal s_{U} over the condition alphabet U = {on, off, auto}.

[figure: t; s_{V} (t); 0; stop; start; 0]

Figure 2.2: Example of an event signal

Figure 2.2 shows an example of an event signal s_{V} over the event alphabet V = {0, start, stop}.

2.2 Condition/Event Systems

Now we define condition/event systems. As said before, such a system is characterized by a relation between input and output signals. The relation can also be seen as a function mapping input signals to sets of output signals. So for each input there may be more than one possible output behavior, but there has to be at least one, since CESs are not allowed to refuse generating output (from a practical point of view, you can always measure some values at the CES’s output “connectors”).

Definition 2.3 (Condition/event system) A quintuple

S = (U, V, Y, Z, S),

is called condition/event system (CES), where

• U is the input condition alphabet,

• V is the input event alphabet,

• Y is the output condition alphabet,

• Z is the output event alphabet, and

• S : C(U) × E(V) → 2^{C(Y)×E(Z)} \ {∅} is the system behavior function.

We also use the symbol S for the system behavior relation R ⊆ Beh(U, V, Y, Z) = C(U) × E(V) × C(Y) × E(Z) with (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ R if and only if (s_{Y} , s_{Z}) ∈ S(s_{U}, s_{V}). □

For the purpose of brevity, we will use the symbols s_{U}, s_{V}, s_{Y}, and s_{Z} to denote the four projections of a given behavior s ∈ Beh(U, V, Y, Z) on its components.

[figure: S; U; V; Y; Z]

Figure 2.3: A block diagram of a condition/event system

Figure 2.3 shows a block diagram of a condition/event system. We use an arrow like \overline{}to denote the flow of a condition signal and \overline{}for an event signal flow. If we need systems with more than these four signals, we use Cartesian products like U = U_{1} × U_{2} as alphabets, and we draw signal flows for each U_{i} in the block diagrams (see, for example, Figure 3.4 on page 34). Formally, we access a certain alphabet U_{i}, its symbols u_{i} ∈ U_{i}, or its signals s_{U_{i}} ∈ C(U_{i}) by using a projection on the ith component of U, (u_{1}, u_{2}) ∈ U, or (s_{U_{1}}, s_{U_{2}}) ∈ C(U).

2.3 Discrete Condition/Event Systems

With the notion of condition/event systems we have introduced a model describing a relation of input and output signals. However, it is in practice very difficult to relate signals, since they range over the infinite time domain ℝ_{≥0}.

Moreover, changes in the condition input might force the CES to generate a proper output event at the time the condition change occurs. This behavior is not intended; only input events should be able to force output events. And since one specifies behaviors over the whole time domain, you can even build systems that are able to look into the future, e.g., a CES that outputs events one time unit before they occur as an input event.

Strange behaviors of such nature can be avoided by demanding certain properties like causality, time-change invariance, and spontaneity [SK91].

Another way of avoiding this, and, which is most important, a way of describing a CES in an operational way, is the model of discrete condition/event systems. These systems communicate with their environment via condition and event signals just like CESs, but an internal finite transition system is used to compute the current output symbols from the current input symbols at each point in time. The input conditions can enable or disable state changes in the transition system, and the input events may force transitions.

Definition 2.4 (Discrete condition/event system) A discrete condition/event system (DCES)

D = (U, V, X, Y, Z, f, g, h, x_{0})

consists of an input condition alphabet U, an input event alphabet V, an output condition alphabet Y, an output event alphabet Z, and

• a finite set X of states,

• a state transition function f : X × U × V → 2^{X} \ {∅},

• a condition output function g : X × U → Y,

• an event output function h : X × X × V → Z, and

• an initial state x_{0} ∈ X. □

We give a short intuitive description of how DCESs work. The formal semantics can be found in Definition 2.7. The function f is used to determine the next state of the transition system. As parameters f has the current state and the current condition and event input symbols. A nonempty set of states is computed by f, and one of these is nondeterministically chosen as the next state. The condition output symbol is generated by g from the current state and input condition symbol. The function h produces the event output symbol; parameters are the current state, the next state (which was chosen from the set of possible ones), and the current event input symbol. Note that g and h allow no nondeterministic choice; this is possible in f only.

Now we introduce two properties which lead to an interesting subclass of DCESs, the well-behaved DCESs.

Definition 2.5 (Well-behaved DCES) Let D be a DCES as in Definition 2.4. D is called well-behaved, if it satisfies

• stuttering: x ∈ f(x, u, 0), and

• output triggering: h(x, x, 0) = 0,

for all x ∈ X and u ∈ U. □

Stuttering describes that the system is always able to stay in the same state as long as no proper input event occurs. This ensures that changes in the input condition cannot force any transitions. Output triggering means that the system does not generate a proper output event if it stays in the same state and no proper input event occurs. This prevents the system from generating infinitely many proper events in finite time, since in a finite time interval only finitely many state changes are allowed (this is required in Definition 2.6 below).

The operative nature of DCESs, well-behavedness, and its semantics (defined below) ensure the properties mentioned above (causality, time-change invariance, spontaneity), which avoid the “strange behaviors”. In the following, we will therefore use well-behaved DCESs only, without explicitly mentioning it. However, when constructing a DCES by giving explicit definitions for f, g, and h, we do have to show that the DCES is well-behaved.

To define the semantics for DCESs, we define runs of DCESs. Intuitively, a run is a function mapping points in time to the state of the DCES’s transition system at that time. A run r always starts at the initial state. At all moments t ∈ ℝ_{≥0}, the value of the condition output signal s_{Y} (t) is computed by g using as parameters the current state r(t) and the current value of the condition input signal s_{U}(t). At each point in time t ∈ ℝ_{>0}, a set of states is generated by f using the last state r(t^{−}), the input condition symbol s_{U}(t^{−}) just before time t, and the current input event symbol s_{V} (t). One of these states is nondeterministically chosen as the new state r(t). The value of the event output signal s_{Z}(t) is computed by h using the last state r(t^{−}), the current state r(t) and the current value of the event input signal s_{V} (t).

Note that nothing is said about the event output symbol at time 0, since the definition of event signal implies s_{Z}(0) = 0.

The usage of s_{U}(t^{−}) as parameter for f emphasizes that conditions cannot force transitions; if the condition input signal changes just at time t, still the old value will be used. So this change can only influence transitions after time t, but not the transition at time t.

Definition 2.6 (Run of a DCES) Let D be a DCES as in Definition 2.4. We call a right-continuous and finite-variable function r : ℝ_{≥0} → X run of D over s ∈ Beh(U, V, Y, Z), if and only the following conditions are satisfied by r:

1. r(t) ∈ f(r(t^{−}), s_{U}(t^{−}), s_{V} (t)) for all t ∈ ℝ_{>0}, 2. s_{Y} (t) = g(r(t), s_{U}(t)) for all t ∈ ℝ_{≥0},

3. s_{Z}(t) = h(r(t^{−}), r(t), s_{V} (t)) for all t ∈ ℝ_{>0}, and

4. r(0) = x_{0}. □

Now we can assign a semantics to DCESs. The semantics of a DCES D is a CES S_{D} with a behavior relation containing all the behaviors matching to possible runs of D.

Definition 2.7 (Semantics of a DCES) Let D be a DCES as in Definition 2.4. The semantics of D is given by the CES S_{D} = (U, V, Y, Z, S_{D}) with s ∈ S_{D} if and only if there exists a run r of D over s, for all s ∈ Beh(U, V, Y, Z). □

There is one crucial question which arises immediately after having defined the semantic relation between CESs and DCESs: Can every condition/event system be described by a discrete condition/event system? Or, speaking formally, can we find for every CES S a DCES D such that S_{D} = S? The answer is obviously no, as shown in the following example.

Example 2.8 We define a simple CES which has only trivial inputs and outputs except for the event output. The only proper output event is a “ping” which can be observed at every time point t ∈ ℕ, i.e., the time difference between two “pings” is exactly one time unit. Let S = (U, V, Y, Z, S) be the CES with the trivial condition alphabets^{2} U = Y = {0}, event alphabets V = {0}, Z = {0, ping}, and, for all s ∈ Beh(U, V, Y, Z),

s ∈ S if and only if s_{Z}(t) = \begin{cases}ping & , if t ∈ ℕ \\ 0 & , otherwise \end{cases} .

Note that the trivial alphabets allow only one possibility for s_{U}, s_{V}, and s_{Y}.

This CES cannot be modeled as a DCES, since DCESs have no means to do quantitative timing. In other words, one can build a DCES that outputs a “ping” from time to time, but there is no way to measure time, so the time difference between two “pings” cannot be forced to be exactly one time unit.

◇

In Chapter 5 we will introduce timed condition/event systems, which are DCESs augmented with timers capable of doing quantitative timing. Using these systems, the behavior above becomes expressible for discrete systems, as we will see in Example 5.9 on page 85.

2In our examples, we use {0} as a trivial condition alphabet. This is quite arbitrary; one can use any singleton U ⊆ D.

22

Connecting Condition/Event Systems

When dealing with a large and complex system in a formal framework like specification languages, programming languages, proof systems, timing diagrams, or, as in this thesis, condition/event systems, it is always a bad idea to treat this system as a whole, i.e., in one monolithic part. Complex systems tend to be unmanageable because of their size and should therefore always be dividable into smaller parts, called modules. This property, called modularity, allows to reuse previously defined modules, to split up work between several teams, and, which is most important, to use compositional reasoning in verification, model checking, and testing. Compositionality [HdR86, HdR90] means that properties of the complex system can be derived from properties of its modules, and that properties of a module are independent from the system it is part of. Compositionality is becoming more and more important, since the growing complexity of systems often makes it impossible to specify, design, or verify a system as a whole due to the state explosion problem. Among other techniques like the use of symbolic representations [HNSY94], compositionality is a promising way to handle large systems.

An important part of a compositional framework is a set of composition operators which describe in a formal way how modules can be connected and how the resulting system can be derived from the modules being parts of the connection. In our framework, we will use the following strategy to examine a connection between CESs or DCESs: First, we define the semantics of a connection among CESs in a descriptive way, that is, we say that a CES S describes the semantics of some connected CESs, if some properties hold. We do not check formally under which circumstances such a CES S exists. In a second step, we define the connection for DCESs in an operational way, that is, we introduce a composition operator for DCESs by saying under which circumstances a DCES D exists such that the semantics of D is the semantics of some connected DCESs, and by giving an effective construction for D. Since the semantics of a DCES is a CES, the semantic reasoning in this second step is based on the descriptive definition in the first step.

In this chapter, we examine several ways of connecting CESs and DCESs. First we have a look at the cascade interconnection and the feedback connection of [SK91]. Then we introduce the loop interconnection, which combines the properties of cascade and feedback. In Chapter 4, we will introduce the parallel interconnection, which is augmented for composing timed condition/event systems in Chapter 5.

3.1 The Cascade Interconnection

The cascade interconnection describes the connection of one system’s outputs with a second system’s inputs as defined in [SK91]. Figure 3.1 shows a cascade interconnection of two CESs. The condition and event alphabets of the connected components have to contain the same symbols. If not all symbols in the input alphabets of S_{2} need to be used in the connecting signals, a less strict definition could allow Y_{1} ⊆ U_{2} and Z_{1} ⊆ V_{2}.

3.1.1 The Cascade Interconnection of C/E Systems

We define a cascade interconnection of two CESs S_{1} and S_{2} as a CES S having the input alphabets of S_{1} and the output alphabets of S_{2}. Intuitively, the behavior of S is given by using the input signals of S as input for S_{1}, the output signals of S_{1} as input for S_{2}, and the output signals of S_{2} as output for S. The signals between S_{1} and S_{2} are not visible in S.

[figure: S_{1}; U_{1}; V_{1}; S_{2}; Y_{2}; Z_{2}; Y_{1} = U_{2}; Z_{1} = V_{2}]

Figure 3.1: CES cascade interconnection of S_{1} and S_{2}

The following definition does not say if such a CES S exists; it only defines if a given CES S is a cascade interconnection of S_{1} and S_{2}.

Definition 3.1 (Cascade interconnection) Let S_{i} = (U_{i}, V_{i}, Y_{i}, Z_{i}, S_{i}) be a CES, i ∈ {1, 2}, with Y_{1} = U_{2} and Z_{1} = V_{2}. A CES S = (U, V, Y, Z, S) is called cascade interconnection of S_{1} and S_{2}, if and only if the following conditions hold:

1. U = U_{1}, V = V_{1}, Y = Y_{2}, Z = Z_{2},

2. S = S_{1} ∘S_{2}, i.e., for any s ∈ Beh(U, V, Y, Z), we have s ∈ S if and only if there exists (s′_{U}, s′_{V}) ∈ S_{1}(s_{U}, s_{V}) such that (s_{Y} , s_{Z}) ∈ S_{2}(s′_{U}, s′_{V}). □

The following lemma states that such a CES S can always be constructed from the given CESs S_{1} and S_{2}.

Lemma 3.2 Given two CESs S_{1} and S_{1} as in Definition 3.1, a CES S can be constructed such that S is a cascade interconnection of S_{1} and S_{2}. □

Proof Let S_{1} and S_{1} be CESs as in Definition 3.1. We define S = (U_{1}, V_{1}, Y_{2}, Z_{2}, S) with s ∈ S if and only if there exists (s′_{U}, s′_{V}) ∈ S_{1}(s_{U}, s_{V}) such that (s_{Y} , s_{Z}) ∈ S_{2}(s′_{U}, s′_{V}), for all s ∈ Beh(U_{1}, V_{1}, Y_{2}, Z_{2}).

Both conditions of Definition 3.1 are obviously fulfilled. It remains to check that S is well-defined, i.e., that for every pair (s_{U}, s_{V}) ∈ C(U_{1})×E(V_{1}) of input signals there exists at least one pair (s_{Y} , s_{Z}) ∈ C(Y_{2}) × E(Z_{2}) of output signals such that (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S. Let (s_{U}, s_{V}) ∈ C(U_{1}) × E(V_{1}). Since S_{1} is well-defined, we find at least one (s′_{U}, s′_{V}) ∈ S_{1}(s_{U}, s_{V}). And since S_{2} is also well-defined, we find at least one (s_{Y} , s_{Z}) ∈ S_{2}(s′_{U}, s′_{V}). By definition of S, this leads to (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S.

3.1.2 The Cascade Interconnection of Discrete C/E Systems

The observation of Lemma 3.2 also holds for DCESs; note that the following theorem makes use of the DCESs’ semantics, since the notion of cascade interconnection in Definition 3.1 is given for CESs only.

Theorem 3.3 Given two DCES D_{i} = (U_{i}, V_{i}, X_{i}, Y_{i}, Z_{i}, f_{i}, g_{i}, h_{i}, x_{0,i}), i ∈ {1, 2}, with Y_{1} = U_{2} and Z_{1} = V_{2}, a DCES D can be effectively constructed such that S_{D} is a cascade interconnection of S_{D_{1}} and S_{D_{2}}. □

The proof of this theorem shows the effective construction of D, which is done as follows: The set of states of D is the Cartesian product of the state sets of D_{1} and D_{2}. The state transitions in the first component of D’s states are the same as in D_{1} using f_{1}. The state transitions in the second component are done like in D_{2}, but the condition and event parameters for f_{2} are the outputs of g_{1} and h_{1}. The condition and event output of D is computed by g_{2} and h_{2}, also using the outputs of g_{1} and h_{1}.

Proof Let D_{1} and D_{2} be given as above. We construct a DCES D such that S_{D} is a cascade interconnection of S_{D_{1}} and S_{D_{2}}. Let D = (U, V, X, Y, Z, f, g, h, x_{0}) be the DCES with U = U_{1}, V = V_{1}, Y = Y_{2}, Z = Z_{2}, X = X_{1} × X_{2}, x_{0} = (x_{0,1}, x_{0,2}), and, for all x = (x_{1}, x_{2}) ∈ X, x′ = (x′_{1}, x′_{2}) ∈ X, u ∈ U, v ∈ V,

• x′ ∈ f(x, u, v) if and only if x′_{1} ∈ f_{1}(x_{1}, u, v) and x′_{2} ∈ f_{2}(x_{2}, g_{1}(x_{1}, u), h_{1}(x_{1}, x′_{1}, v)),

• g(x, u) = g_{2}(x_{2}, g_{1}(x_{1}, u)),

• h(x, x′, v) = h_{2}(x_{2}, x′_{2}, h_{1}(x_{1}, x′_{1}, v)).

It can easily be checked that D is well-behaved, since D_{1} and D_{2} are wellbehaved. Let x = (x_{1}, x_{2}) ∈ X and u ∈ U. Output triggering: h(x, x, 0) = h_{2}(x_{2}, x_{2}, h_{1}(x_{1}, x_{1}, 0)) = h_{2}(x_{2}, x_{2}, 0) = 0. Stuttering: We have x_{1} ∈ f_{1}(x_{1}, u, 0) and x_{2} ∈ f_{2}(x_{2}, g_{1}(x_{1}, u), 0) = f_{2}(x_{2}, g_{1}(x_{1}, u), h_{1}(x_{1}, x_{1}, 0)), so x ∈ f(x, u, 0).

Now we check if S_{D} is a cascade interconnection of S_{D_{1}} and S_{D_{2}}. Condition 1 of Definition 3.1 holds obviously. For proving condition 2, let s ∈ Beh(U, V, Y, Z). We have to show that s ∈ S_{D} if and only if there exists (s′_{U}, s′_{V}) ∈ S_{D_{1}}(s_{U}, s_{V}) such that (s_{Y} , s_{Z}) ∈ S_{D_{2}}(s′_{U}, s′_{V}). We have

s ∈ S_{D}

if and only if (by Definition 2.7)

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r(t) ∈ f(r(t^{−}), s_{U}(t^{−}), s_{V} (t))

2. ∀t ∈ ℝ_{≥0} : s_{Y} (t) = g(r(t), s_{U}(t))

3. ∀t ∈ ℝ_{>0} : s_{Z}(t) = h(r(t^{−}), r(t), s_{V} (t))

4. r(0) = x_{0} if and only if (by construction of f, g, h, and x_{0} of the DCES D)

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1.(a) ∀t ∈ ℝ_{>0} : r(t)_{1} ∈ f_{1}(r(t^{−})_{1}, s_{U}(t^{−}), s_{V} (t))
(b) ∀t ∈ ℝ_{>0} : r(t)_{2} ∈ f_{2}(r(t^{−})_{2}, s′_{U}(t^{−}), s′_{V} (t))
2. ∀t ∈ ℝ_{≥0} : s_{Y} (t) = g_{2}(r(t)_{2}, s′_{U}(t))
3. ∀t ∈ ℝ_{>0} : s_{Z}(t) = h_{2}(r(t^{−})_{2}, r(t)_{2}, s′_{V} (t))
4.(a) r(0)_{1} = x_{0,1}
(b) r(0)_{2} = x_{0,2}

where s′_{U}(t) = g_{1}(r(t)_{1}, s_{U}(t)) s′_{V} (t) = h_{1}(r(t^{−})_{1}, r(t)_{1}, s_{V} (t))

if and only if (we introduce existential quantification for s′_{U} and s′_{V}, and we split r into r_{1} and r_{2})

∃s′_{U} ∈ C(Y_{1}), s′_{V} ∈ E(Z_{1}) :

(a) ∃r_{1} : ℝ_{≥0} → X_{1} (right-continuous, finite-variable) :
1. ∀t ∈ ℝ_{>0} : r_{1}(t) ∈ f_{1}(r_{1}(t^{−}), s_{U}(t^{−}), s_{V} (t))
2. ∀t ∈ ℝ_{≥0} : s′_{U}(t) = g_{1}(r_{1}(t), s_{U}(t))
3. ∀t ∈ ℝ_{>0} : s′_{V} (t) = h_{1}(r_{1}(t^{−}), r_{1}(t), s_{V} (t))
4. r_{1}(0) = x_{0,1}
(b) ∃r_{2} : ℝ_{≥0} → X_{2} (right-continuous, finite-variable) :
1. ∀t ∈ ℝ_{>0} : r_{2}(t) ∈ f_{2}(r_{2}(t^{−}), s′_{U}(t^{−}), s′_{V} (t))
2. ∀t ∈ ℝ_{≥0} : s_{Y} (t) = g_{2}(r_{2}(t), s′_{U}(t))
3. ∀t ∈ ℝ_{>0} : s_{Z}(t) = h_{2}(r_{2}(t^{−}), r_{2}(t), s′_{V} (t))
4. r_{2}(0) = x_{0,2}

if and only if (by Definition 2.7)

∃(s′_{U}, s′_{V}) ∈ S_{D_{1}}(s_{U}, s_{V}) : (s_{Y} , s_{Z}) ∈ S_{D_{2}}(s′_{U}, s′_{V}).

Finally, we can define the cascade interconnection operator for DCESs by using the construction in the previous proof.

Definition 3.4 (Discrete cascade interconnection) Let D_{1} and D_{2} be two DCESs as in Theorem 3.3. The DCES D gained from the construction above is called the discrete cascade interconnection of D_{1} and D_{2}, denoted by D_{1} → D_{2}. □

3.2 The Feedback Connection

In [SK91], the feedback connection describes the connection of one system with itself, i.e., its condition output component is connected to its condition input component, and its event output component is connected to its event input component. The resulting system has no inputs, and the output signals remain visible. Figure 3.2 shows such a feedback connection.

[figure: S; U; V; Y; Z]

Figure 3.2: The feedback connection in [SK91]

Our notion of the feedback connection is slightly different. We have additional input and output components, and the signals in the feedback paths are not visible as output components of the resulting system. They can however be made visible by defining the system in such a way that the feedback signals are copied to the non-feedback components. Figure 3.3 shows a feedback connection of a CES. Like in the cascade interconnection, we demand matching alphabets Y_{2} = U_{2} and Z_{2} = V_{2}. Again, this can be formulated less strict as Y_{2} ⊆ U_{2} and Z_{2} ⊆ V_{2}.

3.2.1 The Feedback Connection of C/E Systems

Given a CES S with all alphabets being a Cartesian product of two single alphabets, we define a feedback connection of S as a CES S′ having as alphabets only the first components of the alphabets of S. Intuitively, the behaviors of S′ are the behaviors s of S restricted to the first components, where we allow only the behaviors s with a feedback solution, i.e., where in the condition, respectively event, signal in the second components of s we have the same signal for both the input and the output part.

As in Definition 3.1, we do not say if such a CES S′ exists; we only define if a given CES S′ is a feedback connection of S.

Definition 3.5 (Feedback connection) Let S = (U_{1} × U_{2}, V_{1} × V_{2}, Y_{1} × Y_{2}, Z_{1} × Z_{2}, S) be a C/E system with Y_{2} = U_{2} and Z_{2} = V_{2}. A C/E system

[figure: S; U_{1}; V_{1}; U_{2}; V_{2}; Y_{1}; Z_{1}; Y_{2}; Z_{2}]

Figure 3.3: CES feedback connection of S

S′ = (U, V, Y, Z, S′) is called feedback connection of S, if and only if the following conditions hold:

1. U = U_{1}, V = V_{1}, Y = Y_{1}, Z = Z_{1},

2. For any s ∈ Beh(U, V, Y, Z), we have s ∈ S′ if and only if there exists s_{Y_{2}} ∈ C(Y_{2}) and s_{Z_{2}} ∈ E(Z_{2}) such that ((s_{U}, s_{Y_{2}}), (s_{V} , s_{Z_{2}}), (s_{Y} , s_{Y_{2}}), (s_{Z}, s_{Z_{2}})) ∈ S. □

In contrast to the cascade interconnection, we cannot find for every CES S with alphabets as in Definition 3.5 a CES S′ which is a feedback connection of S. This is caused by algebraic loops, as shown in the following lemma.

Lemma 3.6 There exists a CES S fulfilling the syntactic requirements of Definition 3.5 having no feedback connection. □

Proof Let S = (U_{1}×U_{2}, V_{1}×V_{2}, Y_{1}×Y_{2}, Z_{1}×Z_{2}, S) be the C/E system with U_{1} = Y_{1} = {0}, V_{1} = V_{2} = Z_{1} = Z_{2} = {0}, U_{2} = Y_{2} = {a, b} and S = {s ∈ Beh(U_{1} ×U_{2}, V_{1} ×V_{2}, Y_{1} ×Y_{2}, Z_{1} ×Z_{2}) | s_{Y_{2}}(t) ≠ s_{U_{2}}(t) for all t ∈ ℝ_{≥0}}. Thus, S has only two non-trivial components, the input and output condition in the feedback part. Since S is defined in such a way that the signals of these components never match (if s_{Y_{2}}(t) = a, then s_{U_{2}}(t) = b and vice versa), we cannot find any s_{Y_{2}} ∈ C(Y_{2}) which meets the requirements in condition 2 of Definition 3.5. So a feedback connection of S must have an empty set of behaviors, which is not allowed for well-defined CESs, see Definition 2.3.

3.2.2 The Feedback Connection of Discrete C/E Systems

Since the CES S given in the proof above can also be modeled as a DCES (see upcoming Example 3.8), it is clear that Lemma 3.6 also holds for DCESs.

So not for every DCES D with alphabets as in Definition 3.5 there exists a DCES D′ such that S_{D′} is a feedback connection of S_{D}.

If we want to define a feedback connection operator for DCESs, we need to have a property that defines for a given DCES D if there exists a DCES D′ with S_{D′} being a feedback connection of S_{D}. Such a property must forbid the existence of algebraic loops in the given DCES D.

In [SK91], where the feedback connection has no additional inputs (see Figure 3.2), this can be done easily be demanding that there exists a solution y for the condition feedback equation y = g(x_{0}, y). Then such a solution y can be used to generate the output condition of D′ by defining g′(x_{0}) = y (remember that D′ has no inputs). Since we have no external input events, stuttering allows us to remain in the initial state x_{0}, and by output triggering, the null event 0 is always a solution for the event feedback. So we have at least one run (always at the initial state x_{0}) of D′ over a behavior that can be regarded as a feedback behavior. However, if there is more than one solution y for the equation y = g(x_{0}, y), only one solution can be used for the initial state, and S_{D′} will only contain a subset of the behaviors of a feedback connection of S_{D} (this is discussed in detail in Example 4.26 on page 67).

Our notion of a feedback connection makes the definition of such a property even more difficult. Since we have additional external inputs, the existence of a solution for the feedback signals may depend on these external input signals. Therefore, we demand for each state of x ∈ X and each external input condition symbol u_{1} ∈ U_{1} that there exists a condition symbol y_{2} ∈ Y_{2} which is a solution for the condition feedback equation, and we demand for each pair of pre- and post-states x, x′ ∈ X and each external input event symbol v_{1} ∈ V_{1} that there exists an event symbol z_{2} ∈ Z_{2} which is a solution for the event feedback equation.

Furthermore, we demand unique solutions, since this makes the construction in the following proof much easier. An operator handling multiple solutions will be presented in Section 4.6.

Theorem 3.7 Given a DCES D = (U_{1} ×U_{2}, V_{1} ×V_{2}, X, Y_{1} ×Y_{2}, Z_{1} ×Z_{2}, f, g, h, x_{0}), with Y_{2} = U_{2} and Z_{2} = V_{2}, a DCES D′ can be effectively constructed such that S_{D′} is a feedback connection of S_{D}, if the following unique solution property holds for D:

• For all x ∈ X and u_{1} ∈ U_{1}, there exists a unique y_{2} ∈ Y_{2} such that g(x, (u_{1}, y_{2}))_{2} = y_{2}.

• For all x, x′ ∈ X and v_{1} ∈ V_{1}, there exists a unique z_{2} ∈ Z_{2} such that h(x, x′, (v_{1}, z_{2}))_{2} = z_{2}. □

Before we prove Theorem 3.7, we present a DCES where the unique solution property does not hold.

Example 3.8 Reconsider the CES S of Lemma 3.6. We define a DCES D which has the CES S as semantics. Let D = (U_{1}×U_{2}, V_{1}×V_{2}, {x}, Y_{1}×Y_{2}, Z_{1}× Z_{2}, f, g, h, x) be the DCES with U_{1} = Y_{1} = {0}, V_{1} = V_{2} = Z_{1} = Z_{2} = {0}, U_{2} = Y_{2} = {a, b} and, for all (u_{1}, u_{2}) ∈ U_{1} × U_{2} and (v_{1}, v_{2}) ∈ V_{1} × V_{2},

• f(x, (u_{1}, u_{2}), (v_{1}, v_{2})) = {x},

• g(x, (u_{1}, u_{2})) = \begin{cases}(0, b), if & u_{2} = a \\ (0, a), if & u_{2} = b \end{cases}, and

• h(x, x, (v_{1}, v_{2})) = (0, 0).

As semantics of D, we have S_{D} = S. Together with Lemma 3.6, this shows that not for every DCES D with alphabets as in Definition 3.5 there exists a DCES D′ such that S_{D′} is a feedback connection of S_{D}.

And since g(x, (0, u_{2}))_{2} ≠ u_{2} follows directly from the definition of g, the unique solution property does not hold. ◇

Now we prove Theorem 3.7. This is done by giving the effective construction of D′, which is done as follows: The set of states of D′ is the set of states of D. The functions f′, g′, and h′ for the state transitions and the condition and event symbol outputs are defined using the functions f, g, and h of D and the unique solutions that have been found while checking the unique solution property.

Proof Let D be given as above, let the unique solution property hold. Let G(x, u_{1}) and H(x, x′, v_{1}) be the unique solutions y_{2} and z_{2}, respectively.

We construct a DCES D′ such that S_{D′} is a feedback connection of S_{D}. Let D′ = (U_{1}, V_{1}, X, Y_{1}, Z_{1}, f′, g′, h′, x_{0}) be the DCES with

• x′ ∈ f′(x, u_{1}, v_{1}) if and only if x′ ∈ f(x, (u_{1}, G(x, u_{1})), (v_{1}, H(x, x′, v_{1}))),

• g′(x, u_{1}) = g(x, (u_{1}, G(x, u_{1})))_{1},

• h′(x, x′, v_{1}) = h(x, x′, (v_{1}, H(x, x′, v_{1})))_{1}, for all x, x′ ∈ X, u_{1} ∈ U_{1}, v_{1} ∈ V_{1}. The DCES D′ is well-behaved, since D is well-behaved, and therefore, H(x, x, 0_{V_{1}}) = 0_{Z_{2}} for all x ∈ X.

Now we check if S_{D′} is a feedback connection of S_{D}. Condition 1 of Definition 3.5 holds obviously. For proving condition 2, let (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ Beh(U_{1}, V_{1}, Y_{1}, Z_{1}). We have to show that (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S_{D′} if and only if there exist s_{Y_{2}} ∈ C(Y_{2}) and s_{Z_{2}} ∈ E(Z_{2}) such that ((s_{U}, s_{Y_{2}}), (s_{V} , s_{Z_{2}}), (s_{Y} , s_{Y_{2}}), (s_{Z}, s_{Z_{2}})) ∈ S_{D}.

We have

(s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S_{D′}

if and only if (by Definition 2.7)

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r(t) ∈ f′(r(t^{−}), s_{U}(t^{−}), s_{V} (t))

2. ∀t ∈ ℝ_{≥0} : s_{Y} (t) = g′(r(t), s_{U}(t))

3. ∀t ∈ ℝ_{>0} : s_{Z}(t) = h′(r(t^{−}), r(t), s_{V} (t))

4. r(0) = x_{0}

if and only if (by construction of the DCES D′)

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r(t) ∈ f(r(t^{−}), \begin{matrix}(s_{U}(t^{−}), G(r(t^{−}), s_{U}(t^{−}))), \\ (s_{V} (t), H(r(t^{−}), r(t), s_{V} (t)))) \end{matrix}

2. ∀t ∈ ℝ_{≥0} : s_{Y} (t) = g(r(t), (s_{U}(t), G(r(t), s_{U}(t))))_{1}

3. ∀t ∈ ℝ_{>0} : s_{Z}(t) = h(r(t^{−}), r(t), (s_{V} (t), H(r(t^{−}), r(t), s_{V} (t))))_{1}

4. r(0) = x_{0}

if and only if (since G and H describe unique signals, they can be replaced by the existentially quantified signals s_{Y_{2}} and s_{Z_{2}})

∃s_{Y_{2}} ∈ C(Y_{2}), s_{Z_{2}} ∈ E(Z_{2}) : ∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r(t) ∈ f(r(t^{−}), (s_{U}(t^{−}), s_{Y_{2}}(t^{−}))), (s_{V} (t), s_{Z_{2}}(t)))

2.a. ∀t ∈ ℝ_{≥0} : s_{Y} (t) = g(r(t), (s_{U}(t), s_{Y_{2}}(t)))_{1}

2.b. ∀t ∈ ℝ_{≥0} : s_{Y_{2}}(t) = g(r(t), (s_{U}(t), s_{Y_{2}}(t)))_{2}

3.a. ∀t ∈ ℝ_{>0} : s_{Z}(t) = h(r(t^{−}), r(t), (s_{V} (t), s_{Z_{2}}(t)))_{1}

3.b. ∀t ∈ ℝ_{>0} : s_{Z_{2}}(t) = h(r(t^{−}), r(t), (s_{V} (t), s_{Z_{2}}(t)))_{2}

4. r(0) = x_{0} if and only if

∃s_{Y_{2}} ∈ C(Y_{2}), s_{Z_{2}} ∈ E(Z_{2}) :

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r(t) ∈ f(r(t^{−}), (s_{U}(t^{−}), s_{Y_{2}}(t^{−}))), (s_{V} (t), s_{Z_{2}}(t)))

2. ∀t ∈ ℝ_{≥0} : (s_{Y} (t), s_{Y_{2}}(t)) = g(r(t), (s_{U}(t), s_{Y_{2}}(t)))

3. ∀t ∈ ℝ_{>0} : (s_{Z}(t), s_{Z_{2}}(t)) = h(r(t^{−}), r(t), (s_{V} (t), s_{Z_{2}}(t)))

4. r(0) = x_{0}

if and only if (by Definition 2.7)

\begin{matrix}∃s_{Y_{2}} ∈ C(Y_{2}), s_{Z_{2}} ∈ E(Z_{2}) : \\ ((s_{U}, s_{Y_{2}}), (s_{V} , s_{Z_{2}}), (s_{Y} , s_{Y_{2}}), (s_{Z}, s_{Z_{2}})) ∈ S_{D}. \end{matrix}

Therefore, condition 2 of Definition 3.5 holds.

Finally, we can define the feedback connection operator for DCESs by using the construction in the previous proof.

Definition 3.9 (Discrete feedback connection) Let D be a DCES as in Theorem 3.7, and let the unique solution property hold. The DCES D′ gained from the construction above is called the discrete feedback connection of D, denoted by D ↩. □

3.3 The Loop Interconnection

The goal of this section is to introduce an interconnection operator which is able to express both the cascade interconnection and the feedback connection. The basic idea is to describe a mutual connection of two systems. Furthermore, each system has its own inputs and outputs for conditions and events. A block diagram of this connection, called loop interconnection, is shown in Figure 3.4. In the connections between the two systems, the condition and event alphabets of the connected components have to be equal, so we demand U_{1,2} = Y_{2,2}, V_{1,2} = Z_{2,2}, U_{2,2} = Y_{1,2}, and V_{2,2} = Z_{1,2}. In a less strict variant, “⊇” instead of “=” can be allowed in all four equations.

[figure: S_{1}; U_{1,1}; V_{1,1}; Y_{1,1}; Z_{1,1}; Z_{1,2}; U_{1,2}; Y_{1,2}; V_{1,2}; S_{2}; U_{2,1}; V_{2,1}; Y_{2,1}; Z_{2,1}; Y_{2,2}; V_{2,2}; Z_{2,2}; U_{2,2}; U; V; Y; Z]

Figure 3.4: CES loop interconnection of S_{1} and S_{2}

3.3.1 The Loop Interconnection of C/E Systems

Given two CESs S_{1} and S_{2} where every alphabet is a Cartesian product of two alphabets, a cascade interconnection of S_{1} and S_{2} is a CES S having as input and output alphabets all the first components of S_{1}’s and S_{2}’s alphabets. The behaviors of S are composed from the first components of the signals in the behaviors of S_{1} and S_{2}, and we demand that the signals of the connections between S_{1} and S_{2} (these are the second components) match. The signals between S_{1} and S_{2} are not visible in S.

Definition 3.10 (Loop interconnection) Let S_{i} = (U_{i}, V_{i}, Y_{i}, Z_{i}, S_{i}) be two C/E systems with inputs U_{i} = U_{i,1} × U_{i,2}, V_{i} = V_{i,1} × V_{i,2}, and outputs Y_{i} = Y_{i,1} × Y_{i,2}, Z_{i} = Z_{i,1} × Z_{i,2}, i ∈ {1, 2}. Let U_{1,2} = Y_{2,2}, V_{1,2} = Z_{2,2}, U_{2,2} = Y_{1,2}, V_{2,2} = Z_{1,2}. A C/E system S = (U, V, Y, Z, S) is called loop interconnection of S_{1} and S_{2}, if and only if the following conditions hold:

1. U = U_{1,1} × U_{2,1}, V = V_{1,1} × V_{2,1}, Y = Y_{1,1} × Y_{2,1}, Z = Z_{1,1} × Z_{2,1}.

2. For all (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ Beh(U, V, Y, Z), we have (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S if and only if there exist s̄_{U_{i}} ∈ C(U_{i,2}), s̄_{V_{i}} ∈ E(V_{i,2}), for i ∈ {1, 2}, such that (((s_{U})_{i}, s̄_{U_{i}}), ((s_{V})_{i}, s̄_{V_{i}}), ((s_{Y})_{i}, s̄_{U_{3−i}}), ((s_{Z})_{i}, s̄_{V_{3−i}})) ∈ S_{i}, for all i ∈ {1, 2}. □

Without proof we state in the following lemma that we cannot find for every two CESs S_{1} and S_{2} with alphabets as in Definition 3.10 a CES S which is a loop interconnection of S_{1} and S_{2}. The reason for this lies again in algebraic loops. An example for this is Figure 1.1 in the introduction.

Lemma 3.11 There exist CESs S_{1} and S_{2} fulfilling the syntactic requirements of Definition 3.10 having no loop interconnection. □

3.3.2 The Loop Interconnection of Discrete C/E Systems

As for the feedback connection, we need a property that defines for two given DCESs D_{1} and D_{2} if there exists a DCES D with S_{D} being a loop interconnection of S_{D_{1}} and S_{D_{2}}. We use again a unique solution property to ensure that there exists a solution for the connections between D_{1} and D_{2}. This time we need as solutions two condition symbols (u_{2,2} for the condition connection from D_{1} to D_{2} and u_{1,2} for the other direction), which depend on the states x_{1} and x_{2} of D_{1} and D_{2} and their external condition input symbols u_{1,1} and u_{2,1}, and two event symbols v_{2,2} and v_{1,2} (one for each event connection between D_{1} and D_{2}), which depend on the pre- and post-states x_{1}, x′_{1} and x_{2}, x′_{2} of D_{1} and D_{2} and their external event input symbols v_{1,1} and v_{2,1}.

Theorem 3.12 Given two DCES D_{i} = (U_{i}, V_{i}, X_{i}, Y_{i}, Z_{i}, f_{i}, g_{i}, h_{i}, x_{0,i}) with inputs U_{i} = U_{i,1}×U_{i,2}, V_{i} = V_{i,1}×V_{i,2}, outputs Y_{i} = Y_{i,1}×Y_{i,2}, Z_{i} = Z_{i,1}×Z_{i,2}, for i ∈ {1, 2}, and matching alphabets U_{1,2} = Y_{2,2}, V_{1,2} = Z_{2,2}, U_{2,2} = Y_{1,2}, V_{2,2} = Z_{1,2}, a DCES D can be effectively constructed such that S_{D} is a loop interconnection of S_{D_{1}} and S_{D_{2}}, if the following unique solution property holds for D_{1} and D_{2}:

• For all x_{1} ∈ X_{1}, x_{2} ∈ X_{2}, u_{1,1} ∈ U_{1,1}, u_{2,1} ∈ U_{2,1}, there exist unique u_{1,2} ∈ U_{1,2}, u_{2,2} ∈ U_{2,2}, such that g_{1}(x_{1}, (u_{1,1}, u_{1,2}))_{2} = u_{2,2} and g_{2}(x_{2}, (u_{2,1}, u_{2,2}))_{2} = u_{1,2}.

• For all x_{1}, x′_{1} ∈ X_{1}, x_{2}, x′_{2} ∈ X_{2}, v_{1,1} ∈ V_{1,1}, v_{2,1} ∈ V_{2,1}, there exist unique v_{1,2} ∈ V_{1,2}, v_{2,2} ∈ V_{2,2}, such that h_{1}(x_{1}, x′_{1}, (v_{1,1}, v_{1,2}))_{2} = v_{2,2} and h_{2}(x_{2}, x′_{2}, (v_{2,1}, v_{2,2}))_{2} = v_{1,2}. □

In the following proof, the effective construction of D is given. The set of states of D is the Cartesian product of the state sets of D_{1} and D_{2}. The functions f, g, and h of D are combined from f_{i}, g_{i}, and h_{i}, i ∈ {1, 2}. The parameters for these functions are taken from the parameters of f, g, and h, and from the unique solutions that have been found while checking the unique solution property.

Proof Let D_{1} and D_{2} be given as above, let the unique solution property hold. Let G_{1}(x_{1}, x_{2}, u_{1,1}, u_{2,1}), G_{2}(x_{1}, x_{2}, u_{1,1}, u_{2,1}), H_{1}(x_{1}, x′_{1}, x_{2}, x′_{2}, v_{1,1}, v_{2,1}), H_{2}(x_{1}, x′_{1}, x_{2}, x′_{2}, v_{1,1}, v_{2,1}) be the unique solutions u_{2,2}, u_{1,2}, v_{2,2}, v_{1,2}, respectively.

We construct a DCES D such that S_{D} is a loop interconnection of S_{D_{1}} and S_{D_{2}}. Let D = (U, V, X, Y, Z, f, g, h, x_{0}) be the DCES with inputs U = U_{1,1} × U_{2,1}, V = V_{1,1} × V_{2,1}, outputs Y = Y_{1,1} × Y_{2,1}, Z = Z_{1,1} × Z_{2,1}, states X = X_{1} × X_{2}, x_{0} = (x_{0,1}, x_{0,2}), and, for all x = (x_{1}, x_{2}) ∈ X, x′ = (x′_{1}, x′_{2}) ∈ X, u = (u_{1,1}, u_{2,1}) ∈ U, v = (v_{1,1}, v_{2,1}) ∈ V,

• x′ ∈ f(x, u, v) if and only if x′_{i} ∈ f_{i}(x_{i}, (u_{i,1}, u_{i,2}), (v_{i,1}, v_{i,2})), i ∈ {1, 2},

• g(x, u) = (g_{1}(x_{1}, (u_{1,1}, u_{1,2}))_{1}, g_{2}(x_{2}, (u_{2,1}, u_{2,2}))_{1}),

• h(x, x′, v) = (h_{1}(x_{1}, x′_{1}, (v_{1,1}, v_{1,2}))_{1}, h_{2}(x_{2}, x′_{2}, (v_{2,1}, v_{2,2}))_{1}),

with

• u_{1,2} = G_{2}(x_{1}, x_{2}, u_{1,1}, u_{2,1}), u_{2,2} = G_{1}(x_{1}, x_{2}, u_{1,1}, u_{2,1}),

• v_{1,2} = H_{2}(x_{1}, x′_{1}, x_{2}, x′_{2}, v_{1,1}, v_{2,1}), v_{2,2} = H_{1}(x_{1}, x′_{1}, x_{2}, x′_{2}, v_{1,1}, v_{2,1}).

It can easily be checked that D is well-behaved, since D_{1} and D_{2} are wellbehaved and therefore, H_{1}(x_{1}, x_{1}, x_{2}, x_{2}, 0_{V_{1,1}}, 0_{V_{2,1}}) = 0_{V_{2,2}} and H_{2}(x_{1}, x_{1}, x_{2}, x_{2}, 0_{V_{1,1}}, 0_{V_{2,1}}) = 0_{V_{1,2}} for all x_{1} ∈ X_{1} and x_{2} ∈ X_{2}.

Now we check if S_{D} is a loop interconnection of S_{D_{1}} and S_{D_{2}}. Condition 1 of Definition 3.10 holds obviously. For proving condition 2, let (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ Beh(U, V, Y, Z). We have to show:

(s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S_{D} if and only if
∃s̄_{U_{i}} ∈ C(U_{i,2}), s̄_{V_{i}} ∈ E(V_{i,2}), for i ∈ {1, 2} :

(((s_{U})_{i}, s̄_{U_{i}}), ((s_{V})_{i}, s̄_{V_{i}}), ((s_{Y})_{i}, s̄_{U_{3−i}}), ((s_{Z})_{i}, s̄_{V_{3−i}})) ∈ S_{D_{i}}, i ∈ {1, 2}.

We have

(s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S_{D}

if and only if (by Definition 2.7)

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r(t) ∈ f(r(t^{−}), s_{U}(t^{−}), s_{V} (t))

2. ∀t ∈ ℝ_{≥0} : s_{Y} (t) = g(r(t), s_{U}(t))

3. ∀t ∈ ℝ_{>0} : s_{Z}(t) = h(r(t^{−}), r(t), s_{V} (t))

4. r(0) = x_{0} if and only if (by construction of the DCES D)

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) : ∀i ∈ {1, 2} :

1. ∀t ∈ ℝ_{>0} : r(t)_{i} ∈ f_{i}(r(t^{−})_{i}, (s_{U}(t^{−})_{i}, u_{i,2}(t^{−})), (s_{V} (t)_{i}, v_{i,2}(t)))

2. ∀t ∈ ℝ_{≥0} : s_{Y} (t)_{i} = g_{i}(r(t)_{i}, (s_{U}(t)_{i}, u_{i,2}(t)))_{1}

3. ∀t ∈ ℝ_{>0} : s_{Z}(t)_{i} = h_{i}(r(t^{−})_{i}, r(t)_{i}, (s_{V} (t)_{i}, v_{i,2}(t)))_{1}

4. r(0)_{i} = x_{0,i} with the unique solutions u_{1,2}(t) = G_{2}(r(t)_{1}, r(t)_{2}, s_{U}(t)_{1}, s_{U}(t)_{2}) u_{2,2}(t) = G_{1}(r(t)_{1}, r(t)_{2}, s_{U}(t)_{1}, s_{U}(t)_{2}) v_{1,2}(t) = H_{2}(r(t^{−})_{1}, r(t)_{1}, r(t^{−})_{2}, r(t)_{2}, s_{V} (t)_{1}, s_{V} (t)_{2}) v_{2,2}(t) = H_{1}(r(t^{−})_{1}, r(t)_{1}, r(t^{−})_{2}, r(t)_{2}, s_{V} (t)_{1}, s_{V} (t)_{2})

if and only if (since u_{1,2}, u_{2,2}, v_{1,2}, v_{2,2} are unique, they can be replaced by the existentially quantified s̄_{U_{1}}, s̄_{U_{2}}, s̄_{V_{1}}, s̄_{V_{2}}, respectively)

∃s̄_{U_{i}} ∈ C(U_{i,2}), s̄_{V_{i}} ∈ E(V_{i,2}), for all i ∈ {1, 2} : ∃r : ℝ_{≥0} → X (right-continuous, finite-variable) : ∀i ∈ {1, 2} :

1. ∀t ∈ ℝ_{>0} : r(t)_{i} ∈ f_{i}(r(t^{−})_{i}, (s_{U}(t^{−})_{i}, s̄_{U_{i}}(t^{−})), (s_{V} (t)_{i}, s̄_{V_{i}}(t)))

2. ∀t ∈ ℝ_{≥0} : s_{Y} (t)_{i} = g_{i}(r(t)_{i}, (s_{U}(t)_{i}, s̄_{U_{i}}(t)))_{1}

3. ∀t ∈ ℝ_{>0} : s_{Z}(t)_{i} = h_{i}(r(t^{−})_{i}, r(t)_{i}, (s_{V} (t)_{i}, s̄_{V_{i}}(t)))_{1}

4. r(0)_{i} = x_{0,i} with s̄_{U_{1}}(t) = G_{2}(r(t)_{1}, r(t)_{2}, s_{U}(t)_{1}, s_{U}(t)_{2}) s̄_{U_{2}}(t) = G_{1}(r(t)_{1}, r(t)_{2}, s_{U}(t)_{1}, s_{U}(t)_{2}) s̄_{V_{1}}(t) = H_{2}(r(t^{−})_{1}, r(t)_{1}, r(t^{−})_{2}, r(t)_{2}, s_{V} (t)_{1}, s_{V} (t)_{2}) s̄_{V_{2}}(t) = H_{1}(r(t^{−})_{1}, r(t)_{1}, r(t^{−})_{2}, r(t)_{2}, s_{V} (t)_{1}, s_{V} (t)_{2}) if and only if (the unique solution property completely determines the behavior of the second components of g_{i} and h_{i})

∃s̄_{U_{i}} ∈ C(U_{i,2}), s̄_{V_{i}} ∈ E(V_{i,2}), for all i ∈ {1, 2} : ∃r : ℝ_{≥0} → X (right-continuous, finite-variable) : ∀i ∈ {1, 2} :

1. ∀t ∈ ℝ_{>0} : r(t)_{i} ∈ f_{i}(r(t^{−})_{i}, (s_{U}(t^{−})_{i}, s̄_{U_{i}}(t^{−})), (s_{V} (t)_{i}, s̄_{V_{i}}(t)))

2. ∀t ∈ ℝ_{≥0} : (s_{Y} (t)_{i}, s̄_{U_{3−i}}(t)) = g_{i}(r(t)_{i}, (s_{U}(t)_{i}, s̄_{U_{i}}(t)))

3. ∀t ∈ ℝ_{>0} : (s_{Z}(t)_{i}, s̄_{V_{3−i}}(t)) = h_{i}(r(t^{−})_{i}, r(t)_{i}, (s_{V} (t)_{i}, s̄_{V_{i}}(t)))

4. r(0)_{i} = x_{0,i}

if and only if (splitting r into r_{1} and r_{2})

∃s̄_{U_{i}} ∈ C(U_{i,2}), s̄_{V_{i}} ∈ E(V_{i,2}), for all i ∈ {1, 2} : ∀i ∈ {1, 2} : ∃r_{i} : ℝ_{≥0} → X_{i} (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r_{i}(t) ∈ f_{i}(r_{i}(t^{−}), (s_{U}(t^{−})_{i}, s̄_{U_{i}}(t^{−})), (s_{V} (t)_{i}, s̄_{V_{i}}(t)))

2. ∀t ∈ ℝ_{≥0} : (s_{Y} (t)_{i}, s̄_{U_{3−i}}(t)) = g_{i}(r_{i}(t), (s_{U}(t)_{i}, s̄_{U_{i}}(t)))

3. ∀t ∈ ℝ_{>0} : (s_{Z}(t)_{i}, s̄_{V_{3−i}}(t)) = h_{i}(r_{i}(t^{−}), r_{i}(t), (s_{V} (t)_{i}, s̄_{V_{i}}(t)))

4. r_{i}(0) = x_{0,i}

if and only if (by Definition 2.7)

\begin{matrix}∃s̄_{U_{i}} ∈ C(U_{i,2}), s̄_{V_{i}} ∈ E(V_{i,2}), for i ∈ \{1, 2\} : \\ (((s_{U})_{i}, s̄_{U_{i}}), ((s_{V})_{i}, s̄_{V_{i}}), ((s_{Y})_{i}, s̄_{U_{3−i}}), ((s_{Z})_{i}, s̄_{V_{3−i}})) ∈ S_{D_{i}}, i ∈ \{1, 2\}. \end{matrix}

Therefore, condition 2 of Definition 3.10 holds.

Now we can define the loop interconnection operator for DCESs by using the construction in the proof above.

Definition 3.13 (Discrete loop interconnection) Let D_{1} and D_{2} be two DCESs as in Theorem 3.12, and let the unique solution property hold. The DCES D gained from the construction above is called the discrete loop interconnection of D_{1} and D_{2}, denoted by D_{1} ↔ D_{2}. □

3.3.3 Properties of the Discrete Loop Interconnection

An interesting observation is that the unique solution property of Theorem 3.12 is independent from the transition functions of D_{1} and D_{2}, and that the two output functions that are constructed for the discrete loop interconnection of D_{1} and D_{2} also does not need the transition functions.

Remark 3.14 The unique solution property for the discrete loop interconnection of the DCESs D_{1} and D_{2} only depends on the condition and event output functions g_{i} and h_{i} of D_{i}, i ∈ {1, 2}, and these functions are sufficient to effectively construct the condition/event output functions of D_{1} ↔ D_{2}. ◇

This observation is useful when checking a large system consisting of several discrete loop interconnections for well-definedness. The following lemma shows this for a connection of three DCESs.

Lemma 3.15 Given three DCESs D_{i} = (U_{i}, V_{i}, X_{i}, Y_{i}, Z_{i}, f_{i}, g_{i}, h_{i}, x_{0,i}) with inputs U_{i} = U_{i,1}×U_{i,2}, V_{i} = V_{i,1}×V_{i,2}, outputs Y_{i} = Y_{i,1}×Y_{i,2}, Z_{i} = Z_{i,1}×Z_{i,2}, for i ∈ {1, 2, 3}, and matching alphabets U_{1,2} = Y_{2,2}, V_{1,2} = Z_{2,2}, U_{2,2} = Y_{1,2}, V_{2,2} = Z_{1,2}, and U_{2,1} = Y_{3,2}, V_{2,1} = Z_{3,2}, U_{3,2} = Y_{2,1}, V_{3,2} = Z_{2,1}, the welldefinedness of (D_{1} ↔ D_{2}) ↔ D_{3} only depends on g_{i} and h_{i}, i ∈ {1, 2, 3}, and these functions are sufficient to effectively construct the condition/event output functions of (D_{1} ↔ D_{2}) ↔ D_{3}. □

Proof Let D_{1}, D_{2}, D_{3} be given as above. Note that the well-definedness reduces to the unique solution property, since the alphabets are chosen to fit to the loop constructions. For checking the well-definedness of (D_{1} ↔ D_{2}) ↔ D_{3}, we first check the well-definedness of D_{1} ↔ D_{2}. By Remark 3.14, this can be done using only g_{1}, h_{1}, g_{2}, h_{2}. If D_{1} ↔ D_{2} is well-defined, we also get from Remark 3.14 that the output functions g_{12} and h_{12} of D_{12} = D_{1} ↔ D_{2} can be effectively constructed from g_{1}, h_{1}, g_{2}, h_{2}. Using Remark 3.14 again, checking the well-definedness of D_{12} ↔ D_{3} can be done by using the functions g_{12}, h_{12}, g_{3}, h_{3} only.

Now, let (D_{1} ↔ D_{2}) ↔ D_{3} be well-defined. We give a direct construction for condition/event output functions g_{123} and h_{123} identical to those of D_{123} = (D_{1} ↔ D_{2}) ↔ D_{3} which only uses g_{i} and h_{i}, i ∈ {1, 2, 3}.

Since the unique solution property holds for D_{1} and D_{2}, we find for all x = (x_{1}, x_{2}, x_{3}) ∈ X_{1} × X_{2} × X_{3}, x′ = (x′_{1}, x′_{2}, x′_{3}) ∈ X_{1} × X_{2} × X_{3}, u_{1} ∈ U_{1,1}, v_{1} ∈ V_{1,1}, u_{2} ∈ U_{3,1}, v_{2} ∈ V_{3,1} unique solutions G_{1}(x, u_{1}, u_{2}), H_{1}(x, x′, v_{1}, v_{2}), and, for all j ∈ {1, 2}, G_{2,j}(x, u_{1}, u_{2}), H_{2,j}(x, x′, v_{1}, v_{2}), and G_{3}(x, u_{1}, u_{2}), H_{3}(x, x′, v_{1}, v_{2}), such that 40 CHAPTER 3. CONNECTING CONDITION/EVENT SYSTEMS

• G_{1}(x, u_{1}, u_{2}) = g_{1}(x_{1}, (u_{1}, G_{2,2}(x, u_{1}, u_{2})))_{2},

• H_{1}(x, x′, v_{1}, v_{2}) = h_{1}(x_{1}, x′_{1}, (v_{1}, H_{2,2}(x, x′, v_{1}, v_{2})))_{2},

• G_{2,j}(x, u_{1}, u_{2}) = g_{2}(x_{2}, (G_{3}(x, u_{1}, u_{2}), G_{1}(x, u_{1}, u_{2})))_{j},

• H_{2,j}(x, x′, v_{1}, v_{2}) = h_{2}(x_{2}, x′_{2}, (H_{3}(x, x′, v_{1}, v_{2}), H_{1}(x, x′, v_{1}, v_{2})))_{j},

• G_{3}(x, u_{1}, u_{2}) = g_{3}(x_{3}, (u_{2}, G_{2,1}(x, u_{1}, u_{2})))_{2},

• H_{3}(x, x′, v_{1}, v_{2}) = h_{3}(x_{3}, x′_{3}, (v_{2}, H_{2,1}(x, x′, v_{1}, v_{2})))_{2}. In the following, we do not distinguish between X_{1} × X_{2} × X_{3} and (X_{1} × X_{2}) × X_{3} for the state space of D_{123}. Let g_{123} and h_{123} be defined by

• g_{123}(x, (u_{1}, u_{2}))_{1} = g_{1}(x_{1}, (u_{1}, G_{2,2}(x, u_{1}, u_{2})))_{1},

• g_{123}(x, (u_{1}, u_{2}))_{2} = g_{3}(x_{3}, (u_{2}, G_{2,1}(x, u_{1}, u_{2})))_{1},

• h_{123}(x, (u_{1}, u_{2}))_{1} = h_{1}(x_{1}, x′_{1}, (v_{1}, H_{2,2}(x, x′, v_{1}, v_{2})))_{1},

• h_{123}(x, (u_{1}, u_{2}))_{2} = h_{3}(x_{3}, x′_{3}, (v_{2}, H_{2,1}(x, x′, v_{1}, v_{2})))_{1}, for all x = (x_{1}, x_{2}, x_{3}) ∈ X_{1} × X_{2} × X_{3}, x′ = (x′_{1}, x′_{2}, x′_{3}) ∈ X_{1} × X_{2} × X_{3}, u_{1} ∈ U_{1,1}, v_{1} ∈ V_{1,1}, u_{2} ∈ U_{3,1}, v_{2} ∈ V_{3,1}.

Let g and h be the condition/event output functions of D_{123}. We prove g_{123} = g and h_{123} = h. Following Definition 3.13, and using G_{1}, H_{1}, G_{2,1}, G_{2,2}, H_{2,1}, H_{2,2}, G_{3}, and H_{3} as the unique solutions in the loop construction, we get for the condition output function

g(x, (u_{1}, u_{2}))_{1} = g_{12}((x_{1}, x_{2}), (u_{1}, G_{3}(x, u_{1}, u_{2})))_{1}
= g_{1}(x_{1}, (u_{1}, G_{2,2}(x, u_{1}, u_{2})))_{1}
= g_{123}(x, (u_{1}, u_{2}))_{1}, and
g(x, (u_{1}, u_{2}))_{2} = g_{3}(x_{3}, (u_{2}, G_{2,1}(x, u_{1}, u_{2})))_{1}
= g_{123}(x, (u_{1}, u_{2}))_{2},

and for the event output function

h(x, x′, (v_{1}, v_{2}))_{1} = h_{12}((x_{1}, x_{2}), (x′_{1}, x′_{2}), (v_{1}, G_{3}(x, x′, v_{1}, v_{2})))_{1}
= h_{1}(x_{1}, x′_{1}, (v_{1}, G_{2,2}(x, x′, v_{1}, v_{2})))_{1}
= h_{123}(x, (v_{1}, v_{2}))_{1}, and
h(x, x′, (v_{1}, v_{2}))_{2} = h_{3}(x_{3}, x′_{3}, (v_{2}, G_{2,1}(x, x′, v_{1}, v_{2})))_{1}
= h_{123}(x, x′, (v_{1}, v_{2}))_{2},

for all x = (x_{1}, x_{2}, x_{3}) ∈ X_{1} × X_{2} × X_{3}, x′ = (x′_{1}, x′_{2}, x′_{3}) ∈ X_{1} × X_{2} × X_{3}, u_{1} ∈ U_{1,1}, v_{1} ∈ V_{1,1}, u_{2} ∈ U_{3,1}, v_{2} ∈ V_{3,1}.

3.3.4 Special Cases of the Discrete Loop Interconnection

Now we show that the discrete loop interconnection operator is able to express the discrete cascade interconnection and the discrete feedback connection.

Theorem 3.16 The discrete cascade interconnection is a special case (modulo some syntactic modifications) of the discrete loop interconnection. □

Proof Let D_{1} and D_{2} be given as in Theorem 3.3. First, we add some trivial input/output components to D_{1} and D_{2}, making them satisfy the syntactic requirements of Theorem 3.12: For i ∈ {1, 2}, let D̄_{i} = (Ū_{i}, V̄_{i}, X_{i}, Ȳ_{i}, Z̄_{i}, f̄_{i}, ḡ_{i}, h̄_{i}, x_{0,i}) be the DCES with

• Ū_{1} = U_{1}×C_{t}, V̄_{1} = V_{1}×E_{t}, Ȳ_{1} = C_{t}×Y_{1}, Z̄_{1} = E_{t}×Z_{1}, and Ū_{2} = C_{t}×U_{2}, V̄_{2} = E_{t} × V_{2}, Ȳ_{2} = Y_{2} × C_{t}, Z̄_{2} = Z_{2} × E_{t}, where C_{t} = {0} is a trivial condition alphabet, and E_{t} = {0} is the trivial event alphabet.

• For all x_{1}, x′_{1} ∈ X_{1}, x_{2}, x′_{2} ∈ X_{2}, u_{1} ∈ U_{1}, u_{2} ∈ U_{2}, v_{1} ∈ V_{1}, v_{2} ∈ V_{2},

– x′_{1} ∈ f̄_{1}(x_{1}, (u_{1}, 0), (v_{1}, 0)) if and only if x′_{1} ∈ f_{1}(x_{1}, u_{1}, v_{1}),

– x′_{2} ∈ f̄_{2}(x_{2}, (0, u_{2}), (0, v_{2})) if and only if x′_{2} ∈ f_{2}(x_{2}, u_{2}, v_{2}),

– ḡ_{1}(x_{1}, (u_{1}, 0)) = (0, g_{1}(x_{1}, u_{1})),

– ḡ_{2}(x_{2}, (0, u_{2})) = (g_{2}(x_{2}, u_{2}), 0),

– h̄_{1}(x_{1}, x′_{1}, (v_{1}, 0)) = (0, h_{1}(x_{1}, x′_{1}, v_{1})),

– h̄_{2}(x_{2}, x′_{2}, (0, v_{2})) = (h_{2}(x_{2}, x′_{2}, v_{2}), 0).

We check the unique solution property for D̄_{1} and D̄_{2}: The second components of ḡ_{2} and h̄_{2} are constant (i. e. there is only trivial feedback from D̄_{2} to D̄_{1}), so it is easy to see that G_{1}(x_{1}, x_{2}, u_{1}, 0) = g_{1}(x_{1}, u_{1}), G_{2}(x_{1}, x_{2}, u_{1}, 0) = 0 and H_{1}(x_{1}, x′_{1}, x_{2}, x′_{2}, v_{1}, 0) = h_{1}(x_{1}, x′_{1}, v_{1}), H_{2}(x_{1}, x′_{1}, x_{2}, x′_{2}, v_{1}, 0) = 0 are the unique solutions.

By using Theorem 3.12, we can effectively construct the discrete loop interconnection D̄ = D̄_{1} ↔ D̄_{2}. By projecting the input and output alphabets of D̄ = (U_{1}×C_{t}, V_{1}×E_{t}, X, C_{t}×Y_{2}, E_{t}×Z_{2}, f̄, ḡ, h̄, (x_{0,1}, x_{0,2})) to its non-trivial components, we get the DCES D = (U_{1}, V_{1}, X, Y_{2}, Z_{2}, f, g, h, (x_{0,1}, x_{0,2})).

Now we check if S_{D} is a cascade interconnection of S_{D_{1}} and S_{D_{2}}. Condition 1 of Definition 3.1 holds obviously. For proving condition 2, let s ∈ Beh(U, V, Y, Z). We have to show that s ∈ S_{D} if and only if there exists (s′_{U}, s′_{V}) ∈ S_{D_{1}}(s_{U}, s_{V}) such that (s_{Y} , s_{Z}) ∈ S_{D_{2}}(s′_{U}, s′_{V}). Let s_{U_{0}} ∈ C(C_{t}), s_{V_{0}} ∈ E(E_{t}). Obviously, s_{U_{0}} and s_{V_{0}} are unique and constant. We have

(s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S_{D}

if and only if (S_{D} is the projection of SD̄ to its non-trivial components)

((s_{U}, s_{U_{0}}), (s_{V} , s_{V_{0}}), (s_{U_{0}}, s_{Y}), (s_{V_{0}}, s_{Z})) ∈ SD̄

if and only if (by Theorem 3.12 and Definition 3.10)

∃s̄_{U_{1}} ∈ C(C_{t}), s̄_{V_{1}} ∈ E(E_{t}), s̄_{U_{2}} ∈ C(U_{2}), s̄_{V_{2}} ∈ E(V_{2}) :
((s_{U}, s̄_{U_{1}}), (s_{V} , s̄_{V_{1}}), (s_{U_{0}}, s̄_{U_{2}}), (s_{V_{0}}, s̄_{V_{2}})) ∈ SD̄_{1},
((s_{U_{0}}, s̄_{U_{2}}), (s_{V_{0}}, s̄_{V_{2}}), (s_{Y} , s̄_{U_{1}}), (s_{Z}, s̄_{V_{1}})) ∈ SD̄_{2}

if and only if (s̄_{U_{1}} and s̄_{V_{1}} are unique and constant, and s̄_{U_{1}} = s_{U_{0}}, s̄_{V_{1}} = s_{V_{0}})

∃s̄_{U_{2}} ∈ C(U_{2}), s̄_{V_{2}} ∈ E(V_{2}) :
((s_{U}, s_{U_{0}}), (s_{V} , s_{V_{0}}), (s_{U_{0}}, s̄_{U_{2}}), (s_{V_{0}}, s̄_{V_{2}})) ∈ SD̄_{1},
((s_{U_{0}}, s̄_{U_{2}}), (s_{V_{0}}, s̄_{V_{2}}), (s_{Y} , s_{U_{0}}), (s_{Z}, s_{V_{0}})) ∈ SD̄_{2}

if and only if (S_{D_{1}} and S_{D_{2}} are the projections of SD̄_{1} and SD̄_{2} to their nontrivial components)

∃s̄_{U_{2}} ∈ C(U_{2}), s̄_{V_{2}} ∈ E(V_{2}) :
(s_{U}, s_{V} , s̄_{U_{2}}, s̄_{V_{2}}) ∈ SD̄_{1},
(s̄_{U_{2}}, s̄_{V_{2}}, s_{Y} , s_{Z}) ∈ SD̄_{2}

if and only if

∃(s′_{u}, s′_{v}) ∈ SD̄_{1}(s_{U}, s_{V}) : (s_{Y} , s_{Z}) ∈ SD̄_{2}(s′_{u}, s′_{v}).

Also the discrete feedback connection is a special case of the discrete loop interconnection. Since feedback involves only one system, we have to add a second system in the proof of the following theorem.

Theorem 3.17 The discrete feedback connection is a special case (modulo some syntactic modifications) of the discrete loop interconnection. □

Proof Let D be given as in Theorem 3.7, and let its unique solution property hold. To model the feedback connection as a loop interconnection, we introduce a second DCES D_{id}.

Let D_{id} = (C_{t} × U_{2}, E_{t} × V_{2}, {x_{id}}, C_{t} × U_{2}, E_{t} × V_{2}, f_{id}, g_{id}, h_{id}, x_{id}) be the DCES with

• f_{id}(x_{id}, u, v) = {x_{id}},

• g_{id}(x_{id}, u) = u, and

• h_{id}(x_{id}, x_{id}, v) = v,

for all u ∈ C_{t} × U_{2}, v ∈ E_{t} × V_{2}, and C_{t} = {0}, E_{t} = {0} being trivial condition/event alphabets. Obviously, D_{id} just copies its input signals to its output signals. So the semantics of D_{id} is

S_{D_{id}} = {(s_{U}, s_{V} , s_{U}, s_{V}) | s_{U} ∈ C(C_{t} × U_{2}), s_{V} ∈ E(E_{t} × V_{2})}.

We check the well-definedness of the loop interconnection D ↔ D_{id}, depicted in Figure 3.5 (compare this with Figures 3.3 and 3.4). It is easy to see that the alphabets match correctly (note that Y_{2} = U_{2} and Z_{2} = V_{2}). The unique solution property for D and D_{id} also holds: Since D_{id} copies from input to output, the unique solutions G_{1}, G_{2}, H_{1}, H_{2} for D and D_{id} are the same as the unique solutions G and H we get from the feedback connection of D.

By using Theorem 3.12, we get the DCES D̄ = D ↔ D_{id}. Projecting the input and output alphabets of D̄ to its non-trivial first components, we get the DCES D′ = (U_{1}, V_{1}, X′, Y_{1}, Z_{1}, f′, g′, h′, x′_{0}).

We check if S_{D′} is a feedback connection of S_{D}. Condition 1 of Definition 3.5 holds obviously. For proving condition 2, let (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ Beh(U_{1}, V_{1}, Y_{1}, Z_{1}). We have to show that (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S_{D′} if and only if there exist s_{Y_{2}} ∈ C(Y_{2}) and s_{Z_{2}} ∈ E(Z_{2}) such that ((s_{U}, s_{Y_{2}}), (s_{V} , s_{Z_{2}}), (s_{Y} , s_{Y_{2}}), (s_{Z}, s_{Z_{2}})) ∈ S_{D}.

Let s_{U_{0}} ∈ C(C_{t}), s_{V_{0}} ∈ E(E_{t}). Obviously, s_{U_{0}} and s_{V_{0}} are unique and constant. We have

(s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S_{D′}

[figure: D; Z_{2}; U_{2}; Y_{2}; V_{2}; D_{id}; C_{t}; E_{t}; C_{t}; E_{t}; U_{2}; V_{2}; V_{2}; U_{2}; U_{1}; V_{1}; Y_{1}; Z_{1}]

Figure 3.5: Modeling feedback of D by loop using the system D_{id}

if and only if (S_{D′} is the projection of SD̄ to its non-trivial components)

((s_{U}, s_{U_{0}}), (s_{V} , s_{V_{0}}), (s_{Y} , s_{U_{0}}), (s_{Z}, s_{V_{0}})) ∈ SD̄

if and only if (by Theorem 3.12 and Definition 3.10)

∃s̄_{U_{1}} ∈ C(U_{2}), s̄_{V_{1}} ∈ E(V_{2}), s̄_{U_{2}} ∈ C(U_{2}), s̄_{V_{2}} ∈ E(V_{2}) :
((s_{U}, s̄_{U_{1}}), (s_{V} , s̄_{V_{1}}), (s_{Y} , s̄_{U_{2}}), (s_{Z}, s̄_{V_{2}})) ∈ S_{D},
((s_{U_{0}}, s̄_{U_{2}}), (s_{V_{0}}, s̄_{V_{2}}), (s_{U_{0}}, s̄_{U_{1}}), (s_{V_{0}}, s̄_{V_{1}})) ∈ S_{D_{id}}

if and only if (from S_{D_{id}}, we conclude s̄_{U_{2}} = s̄_{U_{1}} and s̄_{V_{2}} = s̄_{V_{1}}; we replace them by s_{Y_{2}} and s_{Z_{2}})

∃s_{Y_{2}} ∈ C(U_{2}), s_{Z_{2}} ∈ E(V_{2}) :
((s_{U}, s_{Y_{2}}), (s_{V} , s_{Z_{2}}), (s_{Y} , s_{Y_{2}}), (s_{Z}, s_{Z_{2}})) ∈ S_{D},
((s_{U_{0}}, s_{Y_{2}}), (s_{V_{0}}, s_{Z_{2}}), (s_{U_{0}}, s_{Y_{2}}), (s_{V_{0}}, s_{Z_{2}})) ∈ S_{D_{id}}

if and only if (the last line applies for all s_{Y_{2}} and s_{Z_{2}} and can therefore be removed)

\begin{matrix}∃s_{Y_{2}} ∈ C(U_{2}), s_{Z_{2}} ∈ E(V_{2}) : \\ ((s_{U}, s_{Y_{2}}), (s_{V} , s_{Z_{2}}), (s_{Y} , s_{Y_{2}}), (s_{Z}, s_{Z_{2}})) ∈ S_{D}. \end{matrix}

Now we have reached our goal to present an operator for composing DCESs which is able to express both the cascade interconnection and the feedback connection.

We have seen, however, that the use of these operators involves much work in making different systems syntactically compatible, i.e., we had to introduce new signals over the trivial alphabets C_{t} = {0} and E_{t} = {0}; even new systems like D_{id} had to be created. The following chapter shows how to get rid of this “syntactic sugar”.

46

The Parallel Interconnection

The loop interconnection is the most universal operator for combining condition/event systems we have seen so far. But it has some disadvantages: First, the syntactic requirements for the systems are very strong, as we must have pairs of matching input and output components, even if in some directions we do not have any information to be passed. In that case, we have to add some trivial things, as we can see in the proofs of Theorem 3.16 and Theorem 3.17.

Another disadvantage is that for DCESs D_{1}, D_{2}, and D_{3}, the two terms (D_{1} ↔ D_{2}) ↔ D_{3} and D_{1} ↔ (D_{2} ↔ D_{3}) describe completely different systems. Even if we make adequate syntactic changes to the systems to combine the same components in each expression, one of them may be welldefined, and the other may not, due to different unique solution properties that have to be fulfilled.

This shows that we need a different, more flexible way to describe connections between condition/event systems, and an interconnection operator that is “more distributive” than the loop interconnection. The solution we present is the parallel interconnection, which describes an almost arbitrary connection of CESs, and, by defining the parallel interconnection operator, we are able to do arbitrary connections among DCESs (there are some sensible syntactic restrictions, though).

Connections are described by assigning names to the input and output components of all systems. Components which share the same name are connected. An intuitive semantics for a system of CESs connected in such a way is obvious; For every name occurring in the system, one signal has to be provided. If a name is the name of an output component of a CES, this CES provides the signal for that name, and this signal is used for all input components with that name. If a name is used for input components only, the signal for that name must be an external input signal for the system.

The output signals of the system are the output signals of all CESs. This parallel interconnection of CESs will be given formally in Definition 4.10.

The notion of names makes new definitions for syntax and semantics of CESs and DCESs necessary, but the flexibility we gain for constructing interconnected systems is worth the effort.

4.1 Adding Component Names to C/E Systems

In the previous sections, we described a condition/event system’s inputs and outputs by Cartesian products of condition or event alphabets. We accessed single components by projecting elements of these products on a certain index. To make dealing with many components easier and to provide a natural way of connecting systems, we change the definition of CESs in the following way: All input and output components of a CES are identified by names. Each name is associated with one condition or event alphabet. Each alphabet may be associated with more than one name. Components with the same names are considered to be connected later on.

The following definitions put these considerations on a formal basis. From now on, let N be a global set of identifiers, called names. We associate with each name N ∈ N either a condition or an event alphabet, denoted by α(N). We call N condition name (respectively event name), if α(N) is a condition alphabet (respectively event alphabet).

In Chapter 3, we used Cartesian products of alphabets like U_{1} × U_{2} if a CES or DCES needed to have two independent alphabets in one of its signals. With the new notion of names, we simply use a set of names for such purposes, like for the case above the set Ū = {U_{1}, U_{2}} with α(U_{1}) = U_{1} and α(U_{2}) = U_{2}. We use symbols like U, V, Y, Z for names, and symbols like Ū, V̄, Ȳ, Z̄ for sets of names.

For describing the current value of a system’s component named with the set Ā, we introduce the notion of an evaluation, which is a function mapping the names of Ā to the condition or event symbols in the alphabets associated with the names in Ā.

Definition 4.1 (Evaluation) For a set Ā ⊆ N, we define

ΣĀ = [Ā ⟶^{type} ⋃_{N∈Ā} α(N)]

as the set of all type-preserving functions φ mapping names to conditions or events, where type-preserving in this case means φ(N) ∈ α(N) for all N ∈ Ā. Such a function φ is called evaluation of Ā. □

Note that there is only one evaluation for the empty set of names, and this is the function ∅ having an empty domain, so we have Σ_{∅} = {∅}. If φ(N) = 0_{α(N)} for all N ∈ Ā, we use the symbol 0Ā (or simply 0) for φ. For N ∈ N, we define Σ_{N} as a shortcut for Σ_{{N}}. Furthermore, we define some operations on evaluations.

Definition 4.2 (Operations on evaluations) For evaluations φ and ψ, we define the following operations:

• union: If φ and ψ coincide on the intersection of their domains, φ ∪ ψ denotes their union.

• restriction: For Ā ⊆ dom(φ), the restriction of φ on Ā is denoted by φ|Ā. For the sake of convenient notation, we allow Ā = ∅, resulting in φ|Ā = ∅. For N ∈ N, φ|_{N} is an abbreviation for φ|_{{N}}. □

These operations are extended in the obvious way to named signals and named behaviors, which are defined below.

4.1.1 Named C/E Systems

We use the evaluations introduced above to define named condition/event systems, which operate on named condition/event signals.

Definition 4.3 (Named condition/event signal) Let Ū ⊆ N be a finite set of condition names. A function sŪ : ℝ_{≥0} → ΣŪ is called named condition signal over Ū, if it is right-continuous and finite-variable. The set of all named condition signals over Ū is denoted by C(Ū).

Let V̄ ⊆ N be a finite set of event names. A function sV̄ : ℝ_{≥0} → ΣV̄ is called named event signal over V̄, if sV̄(0) = 0 and in every bounded subinterval I of ℝ_{≥0} there are only finitely many points t ∈ I with sV̄(t) ≠ 0. The set of all named event signals over V̄ is denoted by E(V̄). □

For the signal over an empty set of names we use the symbol ∅, denoting the function s_{∅} : ℝ_{≥0} → Σ_{∅} with constant value ∅.

Now we are ready to define named condition/event systems. We ensure that each name in N is used at most once in one system, since we do not want a system to become connected to itself (feedback will only be allowed by using a second system, as we will see later on).

Definition 4.4 (Named condition/event system) Let Ū and Ȳ be finite sets of condition names, and let V̄ and Z̄ be finite sets of event names. Let all four sets be pairwise disjoint. The quintuple S = (Ū, V̄, Ȳ, Z̄, S) is called named condition/event system, where S : C(Ū) × E(V̄) → 2^{C(Ȳ)×E(Z̄)} \ {∅} is the system behavior function. We also use the symbol S for the system behavior relation R ⊆ Beh(Ū, V̄, Ȳ, Z̄) = C(Ū) × E(V̄) × C(Ȳ) × E(Z̄) with (sŪ, sV̄, sȲ, sZ̄) ∈ R if and only if (sȲ, sZ̄) ∈ S(sŪ, sV̄). □

Sometimes, S_{S} is used to denote the behavior function/relation of the named CES S. For the sake of brevity, we will use the symbols sŪ, sV̄, sȲ, and sZ̄ to denote the four projections of a given s ∈ Beh(Ū, V̄, Ȳ, Z̄) on its components.

4.1.2 Named Discrete C/E Systems

Now we give the definition of named discrete condition/event systems. Note that besides the introduction of names, we now also have a set of initial states instead of only one initial state, because we want to have more than one possibility for the condition output evaluation at time 0. This is discussed in detail in Example 4.26 on page 67.

Definition 4.5 (Named DCES, well-behaved) A named discrete condition/event system D = (Ū, V̄, X, Ȳ, Z̄, f, g, h, X_{0}) consists of

• a finite set Ū of condition input names,

• a finite set V̄ of event input names,

• a finite set Ȳ of condition output names,

• a finite set Z̄ of event output names,

• a finite set X of states,

• a state transition function f : X × ΣŪ × ΣV̄ → 2^{X} \ {∅},

• a condition output function g : X × ΣŪ → ΣȲ,

• an event output function h : X × X × ΣV̄ → ΣZ̄, and

• a nonempty set X_{0} ⊆ X of initial states,

where Ū, V̄, Ȳ, and Z̄ are pairwise disjoint. The named DCES D is called well-behaved, if it satisfies • stuttering: x ∈ f(x, u, 0) and

• output triggering: h(x, x, 0) = 0,

for all x ∈ X and u ∈ ΣŪ. □

In the following we will use well-behaved named DCESs only. To define the semantics for a named DCES, we define runs of named DCESs. Notice that in contrast to Definition 2.6, we have r(0) ∈ X_{0} as start of the run.

Definition 4.6 (Run of a named DCES) Let D be as in Definition 4.5. We call a right-continuous and finite-variable function r : ℝ_{≥0} → X run of D over s ∈ Beh(Ū, V̄, Ȳ, Z̄), if and only if

1. r(t) ∈ f(r(t^{−}), sŪ(t^{−}), sV̄(t)) for all t ∈ ℝ_{>0},

2. sȲ(t) = g(r(t), sŪ(t)) for all t ∈ ℝ_{≥0},

3. sZ̄(t) = h(r(t^{−}), r(t), sV̄(t)) for all t ∈ ℝ_{>0}, and

4. r(0) ∈ X_{0}. □

Now we can assign a semantics to named DCESs. Like in Definition 2.7, it is given via the notion of runs.

Definition 4.7 (Semantics of a named DCES) Let D be as in Definition 4.5. The semantics of D is given by the named CES S_{D} = (Ū, V̄, Ȳ, Z̄, S_{D}) with s ∈ S_{D} if and only if there exists a run r of D over s, for all s ∈ Beh(Ū, V̄, Ȳ, Z̄). □

4.2 The Parallel Interconnection of C/E Systems

Having introduced component names for single condition/event systems, we are now interested in connecting some systems. As mentioned before, all components sharing the same name will be connected to each other.

Figure 4.1 shows an example with three systems (we do not distinguish between conditions and events in this example). The component names of S_{1}, S_{2}, and S_{3} completely determine the connections between them. All outputs of the single systems will become outputs of the composed system, in this case A, D, C, and F. The inputs of the composed system are all inputs of the single systems for which there exist no output of the same name. This results in the input names B and E. Figure 4.2 shows a block diagram of the composed system.

[figure: S_{1}; A; B; B; C; S_{2}; C; A; A; D; D; S_{3}; B; E; E; F; F; C]

Figure 4.1: Example of a parallel interconnection

[figure: S; B; E; A; D; C; F]

Figure 4.2: The composition of the system in Figure 4.1

Remark 4.8 In control theory, there is at least one more possibility to describe connections between systems: One can use a function that describes for each component of a system how this component is connected to other systems. Such functions have some advantages. For example, one can use one name for two different components even if they are not connected. This supports the reuse of modules from a library of systems without having to rename the components.

Though we do not use this method, it is clear that both methods are equally expressive and can be transformed into each other. ◇

In Definition 4.4, we assured that a name is used at most once within one system. For a set of systems to be connected to each other, we also have to ensure that in the whole set of systems all output components must have different names, since outputs must not be connected to each other. This requirement is formalized in the following definition.

Definition 4.9 (Consistent set of named CESs) For i ∈ {1, …, n}, let S_{i} = (Ū_{i}, V̄_{i}, Ȳ_{i}, Z̄_{i}, S_{i}) be a named C/E system. The set {S_{1}, …, S_{n}} is called consistent, if

(Ȳ_{i} ∪ Z̄_{i}) ∩ (Ȳ_{j} ∪ Z̄_{j}) = ∅

holds for all i, j ∈ {1, …, n} with i ≠ j. □

The parallel interconnection of C/E systems can now be defined. This is again only a descriptive definition; we do not reason about the existence of a parallel interconnection for any given set of C/E systems.

Definition 4.10 (Parallel interconnection) For i ∈ {1, …, n}, let S_{i} = (Ū_{i}, V̄_{i}, Ȳ_{i}, Z̄_{i}, S_{i}) be a named C/E system. Let {S_{1}, …, S_{n}} be consistent. A named C/E system S = (Ū, V̄, Ȳ, Z̄, S) is called parallel interconnection of S_{1}, …, S_{n}, if the following conditions hold:

1. The names of the components of S are those of the components of the single systems, except the inputs for which there exists an output with the same name:

Ū = (⋃_{i=1}^{n} Ū_{i}) \ (⋃_{i=1}^{n} Ȳ_{i}) , Ȳ = ⋃_{i=1}^{n} Ȳ_{i},
V̄ = (⋃_{i=1}^{n} V̄_{i}) \ (⋃_{i=1}^{n} Z̄_{i}) , Z̄ = ⋃_{i=1}^{n} Z̄_{i}.

2. For any (sŪ, sV̄, sȲ, sZ̄) ∈ Beh(Ū, V̄, Ȳ, Z̄), we have (sŪ, sV̄, sȲ, sZ̄) ∈ S if and only if there exist (sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}) ∈ S_{i}, for all i ∈ {1, …, n}, such that the following two conditions are satisfied:

(a) Connected components of the single systems share the same signals: For all i, j ∈ {1, …, n} we have

sŪ_{i}|_{Ū_{i}∩Ȳ_{j}} = sȲ_{j}|_{Ū_{i}∩Ȳ_{j}}, and
sV̄_{i}|_{V̄_{i}∩Z̄_{j}} = sZ̄_{j}|_{V̄_{i}∩Z̄_{j}}.

(b) The signals of the single systems match those of S: For all i ∈ {1, …, n} we have

sŪ_{i}|_{Ū_{i}∩Ū} = sŪ|_{Ū_{i}∩Ū}, sȲ_{i} = sȲ|Ȳ_{i}, and sV̄_{i}|_{V̄_{i}∩V̄} = sV̄|_{V̄_{i}∩V̄}, sZ̄_{i} = sZ̄|Z̄_{i}. □

4.3 The Parallel Interconnection of Discrete C/E Systems

In Definition 4.9, we had to ensure that in a set of named CESs which are connected to each other, all output names are different. For discrete systems, this is done analogously in the following definition.

Definition 4.11 (Consistent set of named DCESs) Let D_{i} be a named DCES with component name sets Ū_{i}, V̄_{i}, Ȳ_{i}, and Z̄_{i}, for i ∈ {1, …, n}. The set {D_{1}, …, D_{n}} is called consistent, if

(Ȳ_{i} ∪ Z̄_{i}) ∩ (Ȳ_{j} ∪ Z̄_{j}) = ∅

holds for all i, j ∈ {1, …, n} with i ≠ j. □

For the remainder of this section, let n ∈ ℕ, and, for all i ∈ {1, …, n}, let D_{i} = (Ū_{i}, V̄_{i}, X_{i}, Ȳ_{i}, Z̄_{i}, f_{i}, g_{i}, h_{i}, X_{0,i}) be a named DCES.

The following definition introduces a classification of component names which distinguishes external and internal names.

Definition 4.12 (Component name sets) We define some sets of input and output component names of D_{1}, …, D_{n}:

C^{in} = (⋃_{i=1}^{n} Ū_{i}) \ (⋃_{i=1}^{n} Ȳ_{i}) , E^{in} = (⋃_{i=1}^{n} V̄_{i}) \ (⋃_{i=1}^{n} Z̄_{i}) , C^{io} = (⋃_{i=1}^{n} Ū_{i}) ∩ (⋃_{i=1}^{n} Ȳ_{i}) , E^{io} = (⋃_{i=1}^{n} V̄_{i}) ∩ (⋃_{i=1}^{n} Z̄_{i}) , C^{out} = ⋃_{i=1}^{n} Ȳ_{i} ,  E^{out} = ⋃_{i=1}^{n} Z̄_{i} .  □

The set C^{in} contains all condition input component names for which there exists no output component of that name. These are the names of the condition signals which are not produced within the system; thus, these signals are external and have to be provided by the environment of the compound system. The set C^{io} contains all condition component names for which there exist input and output components of that name. These are the names for the internal condition signals which are exchanged by the systems. The set C^{out} contains all output condition component names (it is a superset of C^{io}). The sets E^{in}, E^{io}, and E^{out} have analog meanings for events. Using the notation of Definition 4.10, we have C^{in} = Ū, E^{in} = V̄, C^{out} = Ȳ, and E^{out} = Z̄.

Looking at the example in Figures 4.1 and 4.2, this definition leads to C^{in} = {B, E}, C^{io} = {A, C}, and C^{out} = {A, C, D, F} (provided we only have conditions).

As for the feedback connection and the loop interconnection of DCESs, we use a unique solution property to ensure that there exists a discrete system with the same semantics as a parallel interconnection of the single systems’ semantics.

Theorem 4.13 Let {D_{1}, …, D_{n}} be consistent. A named DCES D can be effectively constructed such that S_{D} is a parallel interconnection of S_{D_{1}}, …, S_{D_{n}}, if the following unique solution property holds for D_{1}, …, D_{n}:

• For all x_{1} ∈ X_{1}, …, x_{n} ∈ X_{n}, u ∈ Σ_{C^{in}}, there exists a unique y ∈ Σ_{C^{io}} such that for all i ∈ {1, …, n}, we have

g_{i} (x_{i}, (u ∪ y)|Ū_{i}) |_{Ȳ_{i}∩C^{io}} = y|_{Ȳ_{i}∩C^{io}}.

• For all x_{1}, x′_{1} ∈ X_{1}, …, x_{n}, x′_{n} ∈ X_{n}, v ∈ Σ_{E^{in}}, there exists a unique z ∈ Σ_{E^{io}} such that for all i ∈ {1, …, n}, we have

h^{i} (x^{i}, x′i, (v ∪ z)|V̄_{i}) |^{Z̄_{i}∩E^{io}} = z|^{Z̄_{i}∩E^{io}}. □

Before we prove this theorem, we take a look at the possible number of solutions for the evaluations y ∈ C^{io} and z ∈ E^{io}.

Example 4.14 Reconsider the system in Figure 1.1. We define the DCESs D_{1} and D_{2} formally, this time in a parameterized version (cf. Figure 4.3).

D_{1}^{a ↦ a_{1}}^{b ↦ b_{1}}  ^{\overline{}}^{Y_{1}}^{U_{1}} D_{2}^{a ↦ a_{2}}^{b ↦ b_{2}}^{\overline{}}^{U_{2}}^{Y_{2}}

Figure 4.3: Mutually connected DCESs

For i ∈ {1, 2}, let D_{i} = ({U_{i}}, ∅, {x}, {Y_{i}}, ∅, f_{i}, g_{i}, h_{i}, {x}) be a named DCES with α(U_{i}) = α(Y_{i}) = {a, b}, and

• f_{i}(x, u, ∅) = {x} for all u ∈ Σ_{U_{i}},

• g_{i}(x, u)(Y_{i}) = \begin{cases}a_{i}, if & u(U_{i}) = a \\ b_{i}, if & u(U_{i}) = b \end{cases}, and

• h_{i}(x, x, ∅) = ∅.

We have only one state x and empty sets of event names, so the functions f_{i} and h_{i} are constant, and well-definedness is trivially fulfilled.^{1} We characterize the connections between D_{1} and D_{2} by demanding U_{1} = Y_{2} ≠ Y_{1} = U_{2}.

Since D_{1} and D_{2} do not have any event names in common (there are no event names and alphabets at all), we have E^{io} = ∅, and the second condition of unique solution property is trivially fulfilled; the solution is always z = ∅ ∈ Σ_{E^{io}}. Since there are no external condition inputs, we have C^{in} = ∅, and the first condition reduces to finding a unique y ∈ Σ_{{U_{1},U_{2}}} such that

g_{1}(x, y|_{U_{1}}) = y|_{U_{2}} and g_{2}(x, y|_{U_{2}}) = y|_{U_{1}}.

Now consider the following three setups:

1. a_{1} = a, b_{1} = b, and a_{2} = b, b_{2} = a.

2. a_{1} = a, b_{1} = a, and a_{2} = a, b_{2} = a.

3. a_{1} = a, b_{1} = b, and a_{2} = a, b_{2} = b.

For each of the three cases, we take a look at the solutions for the two equations above.

Case 1 has no solutions for y, since the two equations of the unique solution property are contradictory. No DCES D can be given such that S_{D} is a parallel interconnection of S_{D_{1}} and S_{D_{2}}. We have the existence of an algebraic loop; this is the case discussed in the introduction using Figure 1.1.

Case 2 has the unique solution y = {U_{1} ↦ a, U_{2} ↦ a}, and, if Theorem 4.13 is sound, a DCES for the overall system can be effectively constructed, see upcoming Example 4.16.

In case 3 we have two solutions: y = {U_{1} ↦ a, U_{2} ↦ a} and y = {U_{1} ↦ b, U_{2} ↦ b}. Theorem 4.13 does not cover this case, and up to this point we do not know if a suitable DCES exists. At the end of Section 4.6, we will show in Example 4.30 that this is possible. ◇

The previous example could have been formulated using events instead of conditions. But this is a bit more complex, since well-behavedness (output triggering, to be precise) would force us to use at least two states in each DCES, or, if we have only one state, to use an external trigger event. Otherwise, we would not be able to generate any proper output event.

Now we prove Theorem 4.13.

1For output triggering, note that 0_{∅} = ∅ (the evaluation with the empty domain).

Proof Let D_{1}, …, D_{n} be consistent, let the unique solution property hold, and let G(x_{1}, …, x_{n}, u) ∈ Σ_{C^{io}}, respectively, H(x_{1}, …, x_{n}, x′_{1}, …, x′_{n}, v) ∈ Σ_{E^{io}} be the unique solution y, respectively, z, for x_{1}, x′_{1} ∈ X_{1}, …, x_{n}, x′_{n} ∈ X_{n}, u ∈ Σ_{C^{in}}, and v ∈ Σ_{E^{in}}.

We construct a named DCES D such that S_{D} is a parallel interconnection of S_{D_{1}}, …, S_{D_{n}}. Let D = (Ū, V̄, X, Ȳ, Z̄, f, g, h, X_{0}) be the named DCES with component names Ū = C^{in}, V̄ = E^{in}, Ȳ = C^{out}, Z̄ = E^{out}, states X = X_{1} × … × X_{n}, X_{0} = X_{0,1} × … × X_{0,n}, and, for all x = (x_{1}, …, x_{n}) ∈ X, x′ = (x′_{1}, …, x′_{n}) ∈ X, u ∈ ΣŪ, v ∈ ΣV̄,

• x′ ∈ f(x, u, v) if and only if for all i ∈ {1, …, n}:

x′_{i} ∈ f_{i}(x_{i}, (u ∪ G(x, u))|Ū_{i}, (v ∪ H(x, x′, v))|V̄_{i}),

• g(x, u) = ⋃_{i=1}^{n} g_{i}(x_{i}, (u ∪ G(x, u))|Ū_{i}), and

• h(x, x′, v) = ⋃_{i=1}^{n} h_{i}(x_{i}, x′_{i}, (v ∪ H(x, x′, v))|V̄_{i}).

Condition 1 of Definition 4.10 holds obviously by Definition 4.12. For proving condition 2, let (sŪ, sV̄, sȲ, sZ̄) ∈ Beh(Ū, V̄, Ȳ, Z̄). We have

(sŪ, sV̄, sȲ, sZ̄) ∈ S_{D}

if and only if (by Definition 4.7)

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r(t) ∈ f(r(t^{−}), sŪ(t^{−}), sV̄(t))

2. ∀t ∈ ℝ_{≥0} : sȲ(t) = g(r(t), sŪ(t))

3. ∀t ∈ ℝ_{>0} : sZ̄(t) = h(r(t^{−}), r(t), sV̄(t))

4. r(0) ∈ X_{0}

if and only if (by construction of f, g, h, and X_{0} of the named DCES D)

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

∀i ∈ {1, …, n} :

1. ∀t ∈ ℝ_{>0} : r(t)_{i} ∈ f_{i}(r(t^{−})_{i}, \begin{matrix}(sŪ(t^{−}) ∪ G(r(t^{−}), sŪ(t^{−})))|Ū_{i}, \\ (sV̄(t) ∪ H(r(t^{−}), r(t), sV̄(t)))|V̄_{i}) \end{matrix}

2. ∀t ∈ ℝ_{≥0} : sȲ(t)|Ȳ_{i} = g_{i}(r(t)_{i}, (sŪ(t) ∪ G(r(t), sŪ(t)))|Ū_{i})

3. ∀t ∈ ℝ_{>0} : sZ̄(t)|Z̄_{i} = h_{i}(\begin{matrix}r(t^{−})_{i}, r(t)_{i}, \\ (sV̄(t) ∪ H(r(t^{−}), r(t), sV̄(t)))|V̄_{i}) \end{matrix}

4. r(0)_{i} ∈ X_{0,i} if and only if (we split the run r into the runs r_{1}, …, r_{n} (we abbreviate r_{1}(·), …, r_{n}(·) by r̄(·) in the parameters of G and H), and move the signal restrictions into the arguments of the unions)

∃r_{i} : ℝ_{≥0} → X_{i}, for i ∈ {1, …, n} (right-continuous, finite-variable) : ∀i ∈ {1, …, n} :

1. ∀t ∈ ℝ_{>0} :

r_{i}(t) ∈ f_{i}(r_{i}(t^{−}), (sŪ(t^{−})|_{Ū_{i}∩Ū} ∪ G(r̄(t^{−}), sŪ(t^{−}))|_{Ū_{i}∩C^{io}}), (sV̄(t)|_{V̄_{i}∩V̄} ∪ H(r̄(t^{−}), r̄(t), sV̄(t))|_{V̄_{i}∩E^{io}}))

2. ∀t ∈ ℝ_{≥0} : sȲ(t)|Ȳ_{i} = g_{i}(r_{i}(t), (sŪ(t)|_{Ū_{i}∩Ū} ∪ G(r̄(t), sŪ(t))|_{Ū_{i}∩C^{io}}))

3. ∀t ∈ ℝ_{>0} : sZ̄(t)|Z̄_{i} = h_{i}(\begin{matrix}r_{i}(t^{−}), r_{i}(t), \\ (sV̄(t)|_{V̄_{i}∩V̄} ∪ H(r̄(t^{−}), r̄(t), sV̄(t))|_{V̄_{i}∩E^{io}})) \end{matrix}

4. r_{i}(0) ∈ X_{0,i}

if and only if (by Definition 4.7, and by the fact that the unique solutions G and H determine for all systems the signal components with names in C^{io} and E^{io})

∃(sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}) ∈ S_{D_{i}} (for all i ∈ {1, …, n}) :
(a) ∀i, j ∈ {1, …, n} :
sŪ_{i}|_{Ū_{i}∩Ȳ_{j}} = sȲ_{j}|_{Ū_{i}∩Ȳ_{j}},
sV̄_{i}|_{V̄_{i}∩Z̄_{j}} = sZ̄_{j}|_{V̄_{i}∩Z̄_{j}}.
(b) ∀i ∈ {1, …, n} :
sŪ_{i}|_{Ū_{i}∩Ū} = sŪ|_{Ū_{i}∩Ū}, sȲ_{i} = sȲ|Ȳ_{i},
sV̄_{i}|_{V̄_{i}∩V̄} = sV̄|_{V̄_{i}∩V̄}, sZ̄_{i} = sZ̄|Z̄_{i}.

Thus, S_{D} is a parallel interconnection of S_{D_{1}}, …, S_{D_{n}}.

The construction in this proof is the basis for our parallel interconnection operator for DCESs.

Definition 4.15 (Discrete parallel interconnection) Let {D_{1}, …, D_{n}} be consistent, and let the unique solution property of Theorem 4.13 hold. The named DCES D gained from the construction above is called the discrete parallel interconnection of D_{1}, …, D_{n}, denoted by D_{1}∥ … ∥D_{n}. □

In the following example, two small DCESs are composed using the parallel interconnection operator.

Example 4.16 Consider again the DCES D_{1} and D_{2} of Example 4.14. We take a look at case 2, where a_{1} = a, b_{1} = a, and a_{2} = a, b_{2} = a. As stated already, the unique solution property of Theorem 4.13 holds, and the solutions are G(x, ∅) = {U_{1} ↦ a, U_{2} ↦ a} and H(x, x, ∅) = ∅. So we can define

D = D_{1}∥D_{2},

and by Definition 4.15 above and the construction in the proof of Theorem 4.13, we get the DCES D = (∅, ∅, {(x, x)}, Ȳ, ∅, f, g, h, {(x, x)}) with Ȳ = {U_{1}, U_{2}}, α(U_{1}) = α(U_{2}) = {a, b}, and

• f((x, x), ∅, ∅) = {(x, x)},

• g((x, x), ∅) = {U_{1} ↦ a, U_{2} ↦ a}, and

• h((x, x), (x, x), ∅) = ∅.

Thus, D has one state, no inputs, and two condition output components named U_{1} and U_{2}; both deliver constantly the condition symbol a.

There is only one run of D; so by Definition 4.7, we have as formal semantics of D the CES S_{D} = (∅, ∅, Ȳ, ∅, S_{D}) with

S^{D} = {((∅, ∅, sȲ, ∅) | sȲ(t) = {U^{1} ↦ a, U^{2} ↦ a} for all t ∈ ℝ^{≥0}}. ◇

4.4 Hiding Output Components in CESs and DCESs

When using parallel interconnection for system combination, all output signals of the single systems remain visible in the composed system. This is, however, not always desired. Often signals are used for internal communication among a small set of systems, and no other system has these signals as input. When this small set of systems is merged to one system using the parallel interconnection operator, these internal signals become redundant. Our semantics of the parallel interconnection, however, leaves these signals visible. This is comparable to the parallel operator in the language CSP [Hoa85], where the common symbols remain visible after the composition.

For signals that are considered as internal, we would like to have something like in CCS [Mil80, Mil89], where common actions are composed by the parallel operator to an “invisible” action τ, which can be removed later. Therefore, we now provide a hiding operator which simply removes such signals from a system’s output components. We define this operator for named CESs and named DCESs.

Definition 4.17 (CES output component hiding) Let S = (Ū, V̄, Ȳ, Z̄, S) be a named CES, and let N̄ ⊆ N. The output component hiding of N̄ in S, denoted by hide(S, N̄), is defined as the named CES S′ = (Ū, V̄, Ȳ′, Z̄′, S′) with

• Ȳ′ = Ȳ \ N̄, Z̄′ = Z̄ \ N̄, and

• S′ = {(sŪ, sV̄, sȲ|Ȳ′, sZ̄|Z̄′) | (sŪ, sV̄, sȲ, sZ̄) ∈ S}

For N ∈ N, we use hide(S, N) as an abbreviation for hide(S, {N}). □

A semantic characterization of the hiding operator for named CESs is given in the following lemma.

Lemma 4.18 Let S = (Ū, V̄, Ȳ, Z̄, S) be a named CES, and let N̄ ⊆ N. Then, we have

(sŪ, sV̄, sȲ′, sZ̄′) ∈ S_{hide(S,N̄)} ⟺
∃sC̄ ∈ C(Ȳ ∩ N̄), sĒ ∈ E(Z̄ ∩ N̄) : (sŪ, sV̄, sȲ′ ∪ sC̄, sZ̄′ ∪ sĒ) ∈ S

for all (sŪ, sV̄, sȲ′, sZ̄′) ∈ Beh(Ū, V̄, Ȳ \ N̄, Z̄ \ N̄). □

Proof Let S and N̄ be given as above. Let (sŪ, sV̄, sȲ′, sZ̄′) ∈ Beh(Ū, V̄, Ȳ \ N̄, Z̄ \ N̄). We have

(sŪ, sV̄, sȲ′, sZ̄′) ∈ S_{hide(S,N̄)}

if and only if (by Definition 4.17)

(sŪ, sV̄, sȲ′, sZ̄′) ∈ {(sŪ, sV̄, sȲ|_{Ȳ\N̄}, sZ̄|_{Z̄\N̄}) | (sŪ, sV̄, sȲ, sZ̄) ∈ S}

if and only if (by the properties of the restriction operator)

∃sC̄ ∈ C(Ȳ ∩ N̄), sĒ ∈ E(Z̄ ∩ N̄) : (sŪ, sV̄, sȲ′ ∪ sC̄, sZ̄′ ∪ sĒ) ∈ S.

Hiding for discrete condition/event systems is done by restricting the condition and event output functions to the remaining names.

Definition 4.19 (DCES output component hiding) Let D = (Ū, V̄, X, Ȳ, Z̄, f, g, h, X_{0}) be a named DCES, and let N̄ ⊆ N. The output component hiding of N̄ in D, denoted by hide(D, N̄), is defined as the named DCES D′ = (Ū, V̄, X, Ȳ′, Z̄′, f, g′, h′, X_{0}) with • Ȳ′ = Ȳ \ N̄, Z̄′ = Z̄ \ N̄, and

• g′(x, u) = g(x, u)|Ȳ′, h′(x, x′, v) = h(x, x′, v)|Z̄′ for all x, x′, u, v.

For N ∈ N, we use hide(D, N) as an abbreviation for hide(D, {N}). □

By checking Definition 4.5 it is obvious that well-behavedness (stuttering and output triggering) is preserved when applying the hiding operator for DCESs. Furthermore, both versions of the hiding operator have the following properties for all CESs or DCESs S and all N̄, M̄ ∈ N:

• hide(S, N̄) = S, if N̄ ∩ (Ȳ ∪ Z̄) = ∅.

• hide(hide(S, N̄), M̄) = hide(hide(S, M̄), N̄) = hide(S, N̄ ∪ M̄).

Note that the first property also states that input components are not removed.

The semantic connection between the CES version and the DCES version of the hiding operator is given in the following lemma: If we use the semantics of a DCES to transform it into a CES, and we hide some outputs, it makes no difference to the CES whether the hiding is done before or after the transformation.

Lemma 4.20 Let D be a named DCES, and let N̄ ⊆ N. Then we have S_{hide(D,N̄)} = hide(S_{D}, N̄). □

Proof Let D be given as in Definition 4.19, and let N̄ ⊆ N. The component name sets of S_{hide(D,N̄)} and hide(S_{D}, N̄) are obviously equal.

It remains to prove S_{hide(D,N̄)} = S_{hide(S_{D},N̄)}. Let Ȳ′ = Ȳ \ N̄, Z̄′ = Z̄ \ N̄, and let (sŪ, sV̄, sȲ′, sZ̄′) ∈ Beh(Ū, V̄, Ȳ′, Z̄′). We have

(sŪ, sV̄, sȲ′, sZ̄′) ∈ S_{hide(D,N̄)}

if and only if (by Definition 4.19 and Definition 4.7)

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r(t) ∈ f(r(t^{−}), sŪ(t^{−}), sV̄(t))

2. ∀t ∈ ℝ_{≥0} : sȲ′(t) = g(r(t), sŪ(t))|Ȳ′

3. ∀t ∈ ℝ_{>0} : sZ̄′(t) = h(r(t^{−}), r(t), sV̄(t))|Z̄′

4. r(0) ∈ X_{0} if and only if (we introduce the signals sC̄ and sĒ which contain the information hidden by the restriction of g and h)

∃sC̄ ∈ C(Ȳ ∩ N̄), sĒ ∈ E(Z̄ ∩ N̄) :

∃r : ℝ_{≥0} → X (right-continuous, finite-variable) :

1. ∀t ∈ ℝ_{>0} : r(t) ∈ f(r(t^{−}), sŪ(t^{−}), sV̄(t))

2. ∀t ∈ ℝ_{≥0} : (sȲ′ ∪ sC̄)(t) = g(r(t), sŪ(t))

3. ∀t ∈ ℝ_{>0} : (sZ̄′ ∪ sĒ)(t) = h(r(t^{−}), r(t), sV̄(t))

4. r(0) ∈ X_{0}

if and only if (by Definition 4.7)

∃sC̄ ∈ C(Ȳ ∩ N̄), sĒ ∈ E(Z̄ ∩ N̄) : (sŪ, sV̄, sȲ′ ∪ sC̄, sZ̄′ ∪ sĒ) ∈ S_{D}

if and only if (by Lemma 4.18)

(sŪ, sV̄, sȲ′, sZ̄′) ∈ S_{hide(S_{D},N̄)}.

Example 4.21 We show that if we want to express the discrete cascade interconnection by using the discrete parallel interconnection operator, we have to hide the signals between the two DCESs. Let D_{i} = ({U_{i}}, {V_{i}}, X_{i}, {Y_{i}}, {Z_{i}}, f_{i}, g_{i}, h_{i}, X_{0,i}), be a DCES, for i ∈ {1, 2}, with Y_{1} = U_{2} and Z_{1} = V_{2}, and all other names being different (like in Figure 3.1, but with named DCESs instead of unnamed CESs). In a first step, we define

D = D_{1}∥D_{2}.

This operation is well-defined, since the unique solution property of Theorem 4.13 holds; the solutions are just the outputs of D_{1}: G(x_{1}, x_{2}, u) = g_{1}(x_{1}, u) and H(x_{1}, x_{2}, x′_{1}, x′_{2}, v) = h_{1}(x_{1}, x′_{1}, v).

Looking at the sets of output component names in D, we find that they contain Y_{1} and Z_{1}, i.e., the outputs of D_{1} are still visible in D. This does not match our notion of cascade interconnection (Definition 3.1). So we hide these names in D by defining

D′ = hide(D, {Y_{1}, Z_{1}}).

Now S_{D′} is a cascade interconnection of S_{D_{1}} and S_{D_{2}}.

We do not give a formal proof for this, since the next section shows that the discrete parallel interconnection operator is able to express all operators for composing DCES we have seen in Chapter 3 (cascade, feedback, and loop). ◇

4.5 Special Cases of the Discrete Parallel Interconnection

Theorem 4.22 The discrete loop interconnection is a special case of the discrete parallel interconnection (by adding component names and using the hide operator). □

Proof Let D_{i} = (U_{i,1} ×U_{i,2}, V_{i,1} ×V_{i,2}, X_{i}, Y_{i,1} ×Y_{i,2}, Z_{i,1} ×Z_{i,2}, f_{i}, g_{i}, h_{i}, x_{0,i}), i ∈ {1, 2}, be two DCESs with matching alphabets

U_{1,2} = Y_{2,2}, V_{1,2} = Z_{2,2}, and U_{2,2} = Y_{1,2}, V_{2,2} = Z_{1,2}

(cf. Figure 3.4), and let the unique solution property of Theorem 3.12 hold. Since these two DCESs are no named DCESs, we have to introduce names to make the discrete parallel interconnection operator applicable. Therefore, we transform D_{1} and D_{2} to the named DCESs D′_{i} = (Ū_{i}, V̄_{i}, X_{i}, Ȳ_{i}, Z̄_{i}, f′_{i}, g′_{i}, h′_{i}, {x_{0,i}}), i ∈ {1, 2}, with component name sets

Ū_{1} = {U_{1}, C_{2→1}}, V̄_{1} = {V_{1}, E_{2→1}}, Ȳ_{1} = {Y_{1}, C_{1→2}}, Z̄_{1} = {Z_{1}, E_{1→2}},
Ū_{2} = {U_{2}, C_{1→2}}, V̄_{2} = {V_{2}, E_{1→2}}, Ȳ_{2} = {Y_{2}, C_{2→1}}, Z̄_{2} = {Z_{2}, E_{2→2}},

associated alphabets

α(U_{1}) = U_{1,1}, α(V_{1}) = V_{1,1}, α(Y_{1}) = Y_{1,1}, α(Z_{1}) = Z_{1,1},
α(U_{2}) = U_{2,1}, α(V_{2}) = V_{2,1}, α(Y_{2}) = Y_{2,1}, α(Z_{2}) = Z_{2,1},

\begin{matrix}α(C_{2→1}) = U_{1,2} = Y_{2,2}, & α(E_{2→1}) = V_{1,2} = Z_{2,2}, \\ α(C_{1→2}) = U_{2,2} = Y_{1,2}, & α(E_{1→2}) = V_{2,2} = Z_{1,2}, \end{matrix}

for all x, x′ ∈ X_{1}, u ∈ ΣŪ_{1}, v ∈ ΣV̄_{1},

f′_{1}(x, u, v) = f_{1}(x, (u(U_{1}), u(C_{2→1})), (v(V_{1}), v(E_{2→1}))),
g′_{1}(x, u) = g_{1}(x, (u(U_{1}), u(C_{2→1}))),
h′_{1}(x, u, v) = h_{1}(x, x′, (v(V_{1}), v(E_{2→1}))),

and, for all x, x′ ∈ X_{2}, u ∈ ΣŪ_{2}, v ∈ ΣV̄_{2},

f′_{2}(x, u, v) = f_{2}(x, (u(U_{2}), u(C_{1→2})), (v(V_{2}), v(E_{1→2}))),
g′_{2}(x, u) = g_{2}(x, (u(U_{2}), u(C_{1→2}))),
h′_{2}(x, u, v) = h_{2}(x, x′, (v(V_{2}), v(E_{1→2}))).

To make the signals of the unnamed systems and the named systems comparable, we define a function γ mapping evaluations φ of D′_{1} and D′_{2} to pairs of condition or event symbols which can be used by D_{1} and D_{2}:

γ(φ) = \begin{cases}(φ(U_{1}), φ(C_{2→1})), if & φ ∈ ΣŪ_{1} \\ (φ(V_{1}), φ(E_{2→1})), if & φ ∈ ΣV̄_{1} \\ (φ(Y_{1}), φ(C_{1→2})), if & φ ∈ ΣȲ_{1} \\ (φ(Z_{1}), φ(E_{1→2})), if & φ ∈ ΣZ̄_{1} \end{cases} (φ(U_{2}), φ(C_{1→2})), if φ ∈ ΣŪ_{2} (φ(V_{2}), φ(E_{1→2})), if φ ∈ ΣV̄_{2} (φ(Y_{2}), φ(C_{2→1})), if φ ∈ ΣȲ_{2} (φ(Z_{2}), φ(E_{2→1})), if φ ∈ ΣZ̄_{2}

We overload γ in the obvious way to named condition and event signals, and to named behavior sets. With these definitions, it is obvious that γ(S_{D′_{1}}) = S_{D_{1}} and γ(S_{D′_{2}}) = S_{D_{2}}.

Now we are ready to compare the loop and parallel operators. Obviously, {D′_{1}, D′_{2}} is consistent. The unique solution property of Theorem 4.13 also holds for the discrete parallel interconnection of D′_{1} and D′_{2}, since the solutions are those of the loop interconnection. We define the loop interconnection of D_{1} and D_{2}:

D = D_{1} ↔ D_{2},

and we use the parallel interconnection and the hiding operator to define

D′ = hide(D′_{1}∥D′_{2}, {C_{1→2}, E_{1→2}, C_{2→1}, E_{2→1}}).

Note that in D′ we explicitly hide the “internal” signals, while they are hidden implicitly in the construction of D.

It is easy to check that D and D′ have the same input and output alphabets, since the component names of D′ are Ū = {U_{1}, U_{2}}, V̄ = {V_{1}, V_{2}}, Ȳ = {Y_{1}, Y_{2}}, and Z̄ = {Z_{1}, Z_{2}}, which are just the names that remain after hiding the trivial components in the parallel interconnection.

Now we show γ(S_{D′}) = S_{D}. Let (s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ Beh(U_{1,1} × U_{2,1}, V_{1,1} × V_{2,1}, Y_{1,1} × Y_{2,1}, Z_{1,1} × Z_{2,1}). We have

(s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ γ(S_{D′})

if and only if (by definition of γ)

∃(sŪ, sV̄, sȲ, sZ̄) ∈ Beh(Ū, V̄, Ȳ, Z̄) :
γ((sŪ, sV̄, sȲ, sZ̄)) = (s_{U}, s_{V} , s_{Y} , s_{Z}) ∧
(sŪ, sV̄, sȲ, sZ̄) ∈ S_{D′}

if and only if (since D′ = hide(D′_{1}∥D′_{2}, {C_{1→2}, E_{1→2}, C_{2→1}, E_{2→1}}), and by Lemma 4.18 and Lemma 4.20)

∃(sŪ, sV̄, sȲ, sZ̄) ∈ Beh(Ū, V̄, Ȳ, Z̄) : γ((sŪ, sV̄, sȲ, sZ̄)) = (s_{U}, s_{V} , s_{Y} , s_{Z}) ∧ ∃sC̄ ∈ C({C_{1→2}, C_{2→1}}), sĒ ∈ E({E_{1→2}, E_{2→1}}) : (sŪ, sV̄, sȲ ∪ sC̄, sZ̄ ∪ sĒ) ∈ S_{D′_{1}∥D′_{2}}

if and only if (by Definition 4.10, condition 2, and Theorem 4.13)

∃(sŪ, sV̄, sȲ, sZ̄) ∈ Beh(Ū, V̄, Ȳ, Z̄) : γ((sŪ, sV̄, sȲ, sZ̄)) = (s_{U}, s_{V} , s_{Y} , s_{Z}) ∧ ∃sC̄ ∈ C({C_{1→2}, C_{2→1}}), sĒ ∈ E({E_{1→2}, E_{2→1}}) : ∃(sŪ_{1}, sV̄_{1}, sȲ_{1}, sZ̄_{1}) ∈ S_{D′_{1}}, (sŪ_{2}, sV̄_{2}, sȲ_{2}, sZ̄_{2}) ∈ S_{D′_{2}} :

(a) sŪ_{1}|_{C_{2→1}} = sȲ_{2}|_{C_{2→1}}, sŪ_{2}|_{C_{1→2}} = sȲ_{1}|_{C_{1→2}},
sV̄_{1}|_{E_{2→1}} = sZ̄_{2}|_{E_{2→1}}, sV̄_{2}|_{E_{1→2}} = sZ̄_{1}|_{E_{1→2}}
(b) sŪ_{1}|_{U_{1}} = sŪ|_{U_{1}}, sŪ_{2}|_{U_{2}} = sŪ|_{U_{2}},
sV̄_{1}|_{V_{1}} = sV̄|_{V_{1}}, sV̄_{2}|_{V_{2}} = sV̄|_{V_{2}},
sȲ_{1} = (sȲ ∪ sC̄)|Ȳ_{1}, sȲ_{2} = (sȲ ∪ sC̄)|Ȳ_{2},
sZ̄_{1} = (sZ̄ ∪ sĒ)|Z̄_{1}, sZ̄_{2} = (sZ̄ ∪ sĒ)|Z̄_{2}

if and only if (by definition of γ)

∃s̄_{U_{1}} ∈ C(U_{1,2}), s̄_{U_{2}} ∈ C(U_{2,2}), s̄_{V_{1}} ∈ C(V_{1,2}), s̄_{V_{2}} ∈ C(V_{2,2}) : ∃(s_{U}^{1}, s_{V}^{1} , s_{Y}^{1} , s_{Z}^{1}) ∈ γ(S_{D′_{1}}), (s_{U}^{2}, s_{V}^{2} , s_{Y}^{2} , s_{Z}^{2}) ∈ γ(S_{D′_{2}}) :

(a) (s_{U}^{1})_{2} = (s_{Y}^{2} )_{2}, (s_{U}^{2})_{2} = (s_{Y}^{1} )_{2},
(s_{V}^{1} )_{2} = (s_{Z}^{2})_{2}, (s_{V}^{2} )_{2} = (s_{Z}^{1})_{2}
(b) (s_{U}^{1})_{1} = (s_{U})_{1}, (s_{U}^{2})_{1} = (s_{U})_{2},
(s_{V}^{1} )_{1} = (s_{V})_{1}, (s_{V}^{2} )_{1} = (s_{V})_{2},
s_{Y}^{1} = ((s_{Y})_{1}, s̄_{U_{2}}), s_{Y}^{2} = ((s_{Y})_{2}, s̄_{U_{1}}),
s_{Z}^{1} = ((s_{Z})_{1}, s̄_{V_{2}}), s_{Z}^{2} = ((s_{Z})_{2}, s̄_{V_{1}})

if and only if (we have γ(S_{D′_{1}}) = S_{D_{1}} and γ(S_{D′_{2}}) = S_{D_{2}}, and the existentially quantified signals of these systems are completely determined in (a) and (b))

∃s̄_{U_{1}} ∈ C(U_{1,2}), s̄_{V_{1}} ∈ E(V_{1,2}), s̄_{U_{2}} ∈ C(U_{2,2}), s̄_{V_{2}} ∈ E(V_{2,2}) :

(((s_{U})_{1}, s̄_{U_{1}}), ((s_{V})_{1}, s̄_{V_{1}}), ((s_{Y})_{1}, s̄_{U_{2}}), ((s_{Z})_{1}, s̄_{V_{2}})) ∈ S_{D_{1}},

(((s_{U})_{2}, s̄_{U_{2}}), ((s_{V})_{2}, s̄_{V_{2}}), ((s_{Y})_{2}, s̄_{U_{1}}), ((s_{Z})_{2}, s̄_{V_{1}})) ∈ S_{D_{2}} if and only if (by Definition 3.10, D = D_{1} ↔ D_{2}, and Theorem 3.12)

(s_{U}, s_{V} , s_{Y} , s_{Z}) ∈ S_{D}.

Since we already know that the discrete cascade and feedback operators are expressible in terms of the discrete loop operator, we conclude that these operations can also be expressed by the discrete parallel interconnection operator. So we have reached the goal to have one universal operator for all possible ways of connecting discrete condition/event systems.

Theorem 4.23 The discrete cascade interconnection and the discrete feedback connection are special cases of the discrete parallel interconnection. □

Proof This follows with Theorem 4.22 directly from Theorem 3.16 and Theorem 3.17 (cascade and feedback are special cases of loop).

Remark 4.24 If we want to model the feedback connection directly by using the parallel interconnection, we need a second system D_{id} to be inserted in the feedback loop. This system just copies its inputs to its outputs. It is needed because the parallel interconnection operator (the definition of a named (D)CES, actually) does not allow a direct connection from one system to itself. This restriction also ensures that that the application of the unary parallel interconnection operator always results in the original system. ◇

The following example shows how this is done formally.

Example 4.25 Given a DCES D = ({U_{1}, U_{2}}, {V_{1}, V_{2}}, X, {Y_{1}, Y_{2}}, {Z_{1}, Z_{2}}, f, g, h, X_{0}) with α(U_{2}) = α(Y_{2}) and α(V_{2}) = α(Z_{2}), we like to model the discrete feedback connection of D. Since Definition 4.5 does not allow U_{2} = Y_{2} and V_{2} = Z_{2}, we cannot choose the names in that way and simply apply the parallel interconnection operator to D.

Therefore we define a second DCES D_{id} = ({Y_{2}}, {Z_{2}}, {x}, {U_{2}}, {V_{2}}, f_{id}, g_{id}, h_{id}, {x}) by f(x, u, v) = {x}, g(x, u)(U_{2}) = u(Y_{2}), and h(x, x, v)(V_{2}) = v(Z_{2}), for all u ∈ Σ_{Y_{2}}, v ∈ Σ_{Z_{2}}. Obviously, the behavior relation of S_{D_{id}} is

S_{D_{id}} = \begin{cases}(s_{Y_{2}}, s_{Z_{2}}, s_{U_{2}}, s_{V_{2}}) ∈ Beh(\{Y_{2}\}, \{Z_{2}\}, \{U_{2}\}, \{V_{2}\}) | \\ ∀t ∈ ℝ_{≥0} : s_{U_{2}}(t)(U_{2}) = s_{Y_{2}}(t)(Y_{2}) ∧ s_{V_{2}}(t)(V_{2}) = s_{Z_{2}}(t)(Z_{2})\}, \end{cases}

so at each moment, the condition, respectively event, output symbol equals the condition, respectively event, input symbol. A block diagram for the connection of D and D_{id} is shown in Figure 4.4 (compare this with Figure 3.3).

[figure: D; U_{1}; V_{1}; U_{2}; V_{2}; Y_{1}; Z_{1}; Y_{2}; Z_{2}] D_{id}

Figure 4.4: Modeling feedback by parallel using D_{id}

Then we apply the parallel interconnection operator to D and D_{id} and hide the signals between D_{id} and D: D′ = hide(D∥D_{id}, {U_{2}, V_{2}, Y_{2}, Z_{2}}). As result, S_{D′} is a feedback connection of S_{D}. ◇

Since we only allow unique solutions for the values in the feedback loop, the usefulness of this feedback construction is questionable; more interesting systems arise when we allow more than one solution. In the next section, we will redefine the discrete parallel interconnection operator to work with multiple solutions.

4.6 Weakening the Unique Solution Property

Now we want to allow more than one solution for the signals between the systems. Before we start, we show in the following example why we need more than one initial state in DCESs to define a parallel operator with multiple solutions.

Example 4.26 Consider the DCES D = ({U}, ∅, {x}, {Y}, ∅, f, g, h, {x}) with α(U) = α(Y) = {a, b} and, for all u ∈ Σ_{U},

• f(x, u, ∅) = {x},

• g(x, u)(Y) = u(U), and

• h(x, x, ∅) = ∅.

This system has just one state x, no event components, and copies its condition input symbol (which can be a or b) to its condition output. Now we would like to construct a DCES D′ = (∅, ∅, X, {Y}, ∅, f′, g′, h′, X_{0}) which describes the connection of D’s input component U to its output component Y

[figure: D; a ↦ a; b ↦ b; U; Y]

Figure 4.5: A system with two solutions for the feedback value

(this is a feedback connection without events and without external inputs), cf. Figure 4.5.

Since we want multiple solutions this time, the DCES D′ should have a as well as b as a solution for the feedback value. So for all t ∈ ℝ_{≥0}, we want to find both possibilities (∅, ∅, s_{Y}, ∅) ∈ S_{D′} with s_{Y}(t)(Y) = a and (∅, ∅, s_{Y}, ∅) ∈ S_{D′} with s_{Y}(t)(Y) = b.

If we have just one initial state x_{0}, we cannot find both possibilities for time 0. Every run of D′ starts at time 0 with this state x_{0}, leading to s_{Y}(0) = g′(x_{0}, ∅). Since g′ allows no nondeterministic choice, only one value for s_{Y}(0)(Y) is possible.

If we allow two initial states x_{1} and x_{2}, we can define g′(x_{1}, ∅)(Y) = a and g′(x_{2}, ∅)(Y) = b, allowing both solutions for s_{Y}. ◇

For the remainder of this section, let n ∈ ℕ, and, for all i ∈ {1, …, n}, let D_{i} = (Ū_{i}, V̄_{i}, X_{i}, Ȳ_{i}, Z̄_{i}, f_{i}, g_{i}, h_{i}, X_{0,i}) be a named DCES.

Note that the following theorem is the same as Theorem 4.13 except that we do not demand unique solutions.

Theorem 4.27 Let {D_{1}, …, D_{n}} be consistent. A named DCES D can be effectively constructed such that S_{D} is a parallel interconnection of S_{D_{1}}, …, S_{D_{n}}, if the following multiple solution property holds for D_{1}, …, D_{n}:

• For all x_{1} ∈ X_{1}, …, x_{n} ∈ X_{n}, u ∈ Σ_{C^{in}}, there exists a y ∈ Σ_{C^{io}} such that for all i ∈ {1, …, n}, we have

g_{i} (x_{i}, (u ∪ y)|Ū_{i}) |_{Ȳ_{i}∩C^{io}} = y|_{Ȳ_{i}∩C^{io}}.

• For all x_{1}, x′_{1} ∈ X_{1}, …, x_{n}, x′_{n} ∈ X_{n}, v ∈ Σ_{E^{in}}, there exists a z ∈ Σ_{E^{io}} such that for all i ∈ {1, …, n}, we have

h^{i} (x^{i}, x′i, (v ∪ z)|V̄_{i}) |^{Z̄_{i}∩E^{io}} = z|^{Z̄_{i}∩E^{io}}. □

The construction used in the following proof works as follows. Like in the proof of Theorem 4.13, we use a Cartesian product of the sets of states of D_{1}, …, D_{n} as the set of states for the composed system D. The main difference to the unique solution case lies in the selection of the solutions that are used for the functions g and h. If we have more than one possibility for an evaluation of C^{io} or E^{io}, one of these evaluations has to be selected nondeterministically. This selection, however, cannot be done in g or h, since these functions do not allow any nondeterministic choice of output evaluations.

We solve this problem by integrating the nondeterministic choice into f. The Cartesian product in the state space of D is extended by two more sets, one containing all evaluations of C^{io}, and one containing all evaluations of E^{io}. So these two sets contain all possible solutions demanded in the multiple solution property. Now f is constructed in such a way that the last two components of the state (these contain the evaluations) change arbitrarily during each transition; this is where the nondeterministic choice takes place. The output functions g and h can now use these last two components of the state to produce their output. Such an extension of the state space is used by a similar strategy in [SK91] for the feedback connection with multiple solutions.

It may be the case that the evaluation taken from the state’s last two components is not an allowed solution, since all evaluations over C^{io} and E^{io} are contained in the state space, and not every evaluation has to be a solution in each situation. In this case, we fall back on an evaluation which has been picked from the set of solutions beforehand.

Proof Let D_{1}, …, D_{n} be given as above, let the multiple solution property hold, and let G(x, u) ⊆ Σ_{C^{io}}, respectively, H(x, x′, v) ⊆ Σ_{E^{io}} be the sets of solutions y, respectively, z, for x, x′ ∈ X_{1} × … × X_{n}, u ∈ Σ_{C^{in}}, and v ∈ Σ_{E^{in}}. We fix one element of each of the solution sets, and denote it by pick(G(x, u)), respectively, pick(H(x, x′, v)).

We construct a named DCES D such that S_{D} is parallel interconnection of S_{D_{1}}, …, S_{D_{n}}. Let D = (Ū, V̄, X, Ȳ, Z̄, f, g, h, X_{0}) be the named DCES with

• component names Ū = C^{in}, V̄ = E^{in}, Ȳ = C^{out}, Z̄ = E^{out},

• states X = X_{1} × … × X_{n} × Σ_{C^{io}} × Σ_{E^{io}},

• initial states X_{0} = X_{0,1} × … × X_{0,n} × Σ_{C^{io}} × Σ_{E^{io}},

and, for all states x = (x_{1}, …, x_{n}, y, z) ∈ X, x′ = (x′_{1}, …, x′_{n}, y′, z′) ∈ X, input condition evaluations u ∈ ΣŪ, and input event evaluations v ∈ ΣV̄ (we use x̄, resp. x̄′, as an abbreviation for (x_{1}, …, x_{n}), resp. (x′_{1}, …, x′_{n})), • x′ ∈ f(x, u, v) if and only x′_{i} ∈ f_{i}(x_{i}, (u∪g(x, u))|Ū_{i}, (v∪h(x, x′, v))|V̄_{i}),

for all i ∈ {1, …, n} (note that there are no restrictions to y′ and z′; they are selected arbitrarily),

• g(x, u) = ⋃_{i=1}^{n} g_{i}(x_{i}, (u ∪ ŷ(x, u))|Ū_{i}),

where ŷ(x, u) = \begin{cases}y & , if y ∈ G(x̄, u) \\ pick(G(x̄, u)) & , if y ∉ G(x̄, u) \end{cases}, and

• h(x, x′, v) = ⋃_{i=1}^{n} h_{i}(x_{i}, x′_{i}, (v ∪ ẑ(x, x′, v))|V̄_{i}), where ẑ(x, x′, v)

= \begin{cases}0 & , if (x = x′) ∧ (v = 0) \\ z′ & , if ((x ≠ x′) ∨ (v ≠ 0)) ∧ z′ ∈ H(x̄, x̄′, v) \\ pick(H(x̄, x̄′, v)) & , if ((x ≠ x′) ∨ (v ≠ 0)) ∧ z′ ∉ H(x̄, x̄′, v) \end{cases}.

Note that pick(·) has been fixed initially; so there is no nondeterministic choice in g or h (this takes place in f). Further note that the unions in the definitions of g and h are well-defined, since {D_{1}, …, D_{n}} is consistent and therefore, there is no interference of the single systems’ output functions.

We show that D is well-behaved. Let x = (x_{1}, …, x_{n}, y, z) ∈ X, u ∈ ΣŪ. Output triggering: We have to show that h(x, x, 0) = 0. Since all D_{i} are well-behaved (output triggering), we have

h(x, x, 0V̄) = ⋃_{i=1}^{n} h_{i}(x_{i}, x_{i}, (0V̄ ∪ ẑ(x, x, 0V̄))|V̄_{i})
= ⋃_{i=1}^{n} h_{i}(x_{i}, x_{i}, (0V̄ ∪ 0_{E^{io}})|V̄_{i})
= ⋃_{i=1}^{n} h_{i}(x_{i}, x_{i}, 0V̄_{i}) = ⋃_{i=1}^{n} 0Z̄_{i} = 0Z̄.

Stuttering: We have to show that x ∈ f(x, u, 0). Let i ∈ {1, …, n}. Since D_{i} is well-behaved (stuttering) and h(x, x, 0) = 0 (see above), we have

\begin{aligned}x_{i} & ∈ & f_{i}(x_{i}, (u ∪ g(x, u))|Ū_{i}, 0V̄_{i}) \\ & = & f_{i}(x_{i}, (u ∪ g(x, u))|Ū_{i}, (0V̄ ∪ h(x, x, 0V̄))|V̄_{i}). \end{aligned}

So D is well-behaved.

Now we prove that S_{D} is a parallel interconnection of S_{D_{1}}, …, S_{D_{n}}. Condition 1 of Definition 4.10 holds obviously by Definition 4.12. For proving condition 2, let (sŪ, sV̄, sȲ, sZ̄) ∈ Beh(Ū, V̄, Ȳ, Z̄).

First we prove the implication from left to right. Let (sŪ, sV̄, sȲ, sZ̄) ∈ S_{D}.

This implies by Definition 4.7 that we have a run r : ℝ_{≥0} → X (rightcontinuous, finite-variable) of D such that

1. r(t) ∈ f(r(t^{−}), sŪ(t^{−}), sV̄(t)) for all t ∈ ℝ_{>0},
2. sȲ(t) = g(r(t), sŪ(t))  for all t ∈ ℝ_{≥0},
3. sZ̄(t) = h(r(t^{−}), r(t), sV̄(t)) for all t ∈ ℝ_{>0}, and

4. r(0) ∈ X_{0}.

We construct the signals for the single systems, which are existentially quantified in condition 2 of Definition 4.10. For all i ∈ {1, …, n}, let

sŪ_{i} = (sŪ ∪ sȲ)|Ū_{i}, sV̄_{i} = (sV̄ ∪ sZ̄)|V̄_{i}, sȲ_{i} = sȲ|Ȳ_{i}, sZ̄_{i} = sZ̄|Z̄_{i}.

Conditions 2(a) and 2(b) of Definition 4.10 are fulfilled obviously.

It remains to prove (sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}) ∈ S_{D_{i}} for all i ∈ {1, …, n}. Let i ∈ {1, …, n}. We project the run r of D on its ith component to get a run of D_{i}: Define r_{i} : ℝ_{≥0} → X_{i} by r_{i}(t) = r(t)_{i} for all t ∈ ℝ_{≥0}. Obviously, r_{i} is right-continuous and finite-variable, since r is. For proving that r_{i} really is a run of D_{i} over (sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}), we have to show

1. r_{i}(t) ∈ f_{i}(r_{i}(t^{−}), sŪ_{i}(t^{−}), sV̄_{i}(t)) for all t ∈ ℝ_{>0},
2. sȲ_{i}(t) = g_{i}(r_{i}(t), sŪ_{i}(t))  for all t ∈ ℝ_{≥0},
3. sZ̄_{i}(t) = h_{i}(r_{i}(t^{−}), r_{i}(t), sV̄_{i}(t)) for all t ∈ ℝ_{>0}, and

4. r_{i}(0) ∈ X_{0,i}.

Claim 1 holds: For all t ∈ ℝ_{>0}, we have

r_{i}(t) = r(t)_{i} ∈ f(r(t^{−}), sŪ(t^{−}), sV̄(t))_{i}
= f_{i}(r(t^{−})_{i}, \begin{matrix}(sŪ(t^{−}) ∪ g(r(t^{−}), sŪ(t^{−})))|Ū_{i}, \\ (sV̄(t) ∪ h(r(t^{−}), r(t), sV̄(t)))|V̄_{i}) \end{matrix}

= f_{i}(r(t^{−})_{i}, (sŪ(t^{−}) ∪ sȲ(t^{−}))|Ū_{i}, (sV̄(t) ∪ sZ̄(t))|V̄_{i})
= f_{i}(r_{i}(t^{−}), sŪ_{i}(t^{−}), sV̄_{i}(t)).

Claim 2 holds: For all t ∈ ℝ_{≥0}, we have

sȲ_{i}(t) = sȲ(t)|Ȳ_{i} = g(r(t), sŪ(t))|Ȳ_{i}
= g_{i}(r(t)_{i}, (sŪ(t) ∪ ŷ(r(t), sŪ(t)))|Ū_{i})
= g_{i}(r(t)_{i}, (sŪ(t) ∪ sȲ(t))|Ū_{i})
= g_{i}(r_{i}(t), sŪ_{i}(t)).

In the equation above, the multiple solution property and ŷ(r(t), sŪ(t)) being one of the solutions implies ŷ(r(t), sŪ(t))|_{Ū_{i}∩C^{io}} = sȲ(t)|_{Ū_{i}∩C^{io}}.

Claim 3 holds: For all t ∈ ℝ_{>0}, we have

sZ̄_{i}(t) = sZ̄(t)|Z̄_{i} = h(r(t^{−}), r(t), sV̄(t))|Z̄_{i}
= h_{i}(r(t^{−})_{i}, r(t)_{i}, (sV̄(t) ∪ ẑ(r(t^{−}), r(t), sV̄(t)))|V̄_{i})
= h_{i}(r(t^{−})_{i}, r(t)_{i}, (sV̄(t) ∪ sZ̄(t))|V̄_{i})
= h_{i}(r_{i}(t^{−}), r_{i}(t), sV̄_{i}(t)).

In the equation above, the multiple solution property and ẑ(r(t^{−}), r(t), sV̄(t)) being one of the solutions implies ẑ(r(t^{−}), r(t), sV̄(t))|_{V̄_{i}∩E^{io}} = sZ̄(t)|_{V̄_{i}∩E^{io}}.

Claim 4 holds: r_{i}(0) = r(0)_{i} ∈ (X_{0})_{i} = X_{0,i}.

So r_{i} is a run of D_{i} over (sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}). Thus, (sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}) ∈ S_{D_{i}} for all i ∈ {1, …, n}.

Now we prove the implication from right to left. Let (sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}) ∈ S_{D_{i}}, for all i ∈ {1, …, n}, such that conditions 2(a) and 2(b) of Definition 4.10 hold. By Definition 4.7, we find for all i ∈ {1, …, n} a run r_{i} : ℝ_{≥0} → X_{i} (right-continuous, finite-variable) of D_{i} such that

1. r_{i}(t) ∈ f_{i}(r_{i}(t^{−}), sŪ_{i}(t^{−}), sV̄_{i}(t)) for all t ∈ ℝ_{>0},
2. sȲ_{i}(t) = g_{i}(r_{i}(t), sŪ_{i}(t))  for all t ∈ ℝ_{≥0},
3. sZ̄_{i}(t) = h_{i}(r_{i}(t^{−}), r_{i}(t), sV̄_{i}(t)) for all t ∈ ℝ_{>0}, and

4. r_{i}(0) ∈ X_{0,i}.

We use the runs r_{i} and the signals sȲ and sZ̄ to construct a run r of D. The main difficulty lies in the construction of r_{n+2}, i.e., the component which suggests the event evaluations for E^{io}. It would be easy just to define r_{n+2} = sZ̄|_{E^{io}}, but if there exists a t ∈ ℝ_{>0} with sZ̄|_{E^{io}}(t) ≠ 0, r_{n+2} would not be right-continuous at t, and r would be no run. Therefore, we define r_{n+2}(t) = sZ̄|_{E^{io}}(t) for all t ∈ ℝ_{>0} with sZ̄(t) ≠ 0, but we also prolong each proper event symbol in r_{n+2} for a finite amount of time ε > 0, i.e., r_{n+2}(t + x) = sZ̄|_{E^{io}}(t) for all x ∈ [0, ε). This ε must be small enough not to interfere with other events or transitions taking place.

This needs some preparation. Let d_{0}, d_{1}, … be the strictly ordered finite or infinite sequence of all discontinuity points of sV̄, sZ̄, and r_{i}, for all i ∈ {1, …, n}. Note that for any bounded subinterval of ℝ_{≥0}, there are only finitely many d_{j} contained in it. So the d_{j} are all the points in time where we make a transition in one of the single systems or receive a proper input event or generate a proper output event.

Now define r : ℝ_{≥0} → X by r(t) = (r_{1}(t), …, r_{n}(t), y(t), z(t)) with • y(t) = sȲ(t)|_{C^{io}}, and

• z(t) = \begin{cases}sZ̄(d_{j})|_{E^{io}} & , if t ∈ [d_{j}, \frac{d_{j}+d_{j+1}}{2} ) for a j ∈ ℕ \\ 0_{E^{io}} & , otherwise \end{cases},

for all t ∈ ℝ_{≥0}. Note that z is right-continuous and finite-variable, and that for all d_{j}, we have z(d_{j}) = sZ̄(d_{j})|_{E^{io}}, and, if sZ̄(d_{j}) ≠ 0, we have z(d_{j}^{−}) = 0, i.e., d_{j} is a discontinuity point of z. Obviously, r is right-continuous and finite-variable, since all r_{i} and sȲ are, and since z is by construction.

Now we prove that r is a run of D over (sŪ, sV̄, sȲ, sZ̄). We have to show:

1. r(t) ∈ f(r(t^{−}), sŪ(t^{−}), sV̄(t)) for all t ∈ ℝ_{>0},
2. sȲ(t) = g(r(t), sŪ(t))  for all t ∈ ℝ_{≥0},
3. sZ̄(t) = h(r(t^{−}), r(t), sV̄(t)) for all t ∈ ℝ_{>0}, and

4. r(0) ∈ X_{0}.

Claim 4 holds:

r(0) \begin{matrix}= (r_{1}(0), …, r_{n}(0), y(0), z(0)) \\ ∈ X_{0,1} × … × X_{0,n} × Σ_{C^{io}} × Σ_{E^{io}} = X_{0}. \end{matrix}

Claim 2 holds: Let t ∈ ℝ_{≥0}. We have y(t) ∈ G(r̄(t), sŪ(t)), since for all i ∈ {1, …, n} the solution property holds for y(t):

g_{i}(r_{i}(t), (sŪ(t) ∪ y(t))|_{Ȳ_{i}∩C^{io}})|_{Ȳ_{i}∩C^{io}}
= g_{i}(r_{i}(t), (sŪ(t) ∪ sȲ(t)|_{C^{io}})|_{Ȳ_{i}∩C^{io}})|_{Ȳ_{i}∩C^{io}}
= g_{i}(r_{i}(t), sŪ_{i}(t))|_{Ȳ_{i}∩C^{io}}
= sȲ_{i}(t)|_{Ȳ_{i}∩C^{io}} = sȲ(t)|_{Ȳ_{i}∩C^{io}} = y(t)|_{Ȳ_{i}∩C^{io}}.

So ŷ(r(t), sŪ(t)) = y(t), yielding

sȲ(t) = ⋃_{i=1}^{n} sȲ_{i}(t) = ⋃_{i=1}^{n} g_{i}(r_{i}(t), sŪ_{i}(t))
= ⋃_{i=1}^{n} g_{i}(r_{i}(t), (sŪ(t) ∪ sȲ(t))|Ū_{i})
= ⋃_{i=1}^{n} g_{i}(r_{i}(t), sŪ(t)|_{Ū_{i}∩C^{in}} ∪ sȲ(t)|_{Ū_{i}∩C^{io}})
= ⋃_{i=1}^{n} g_{i}(r_{i}(t), sŪ(t)|_{Ū_{i}∩C^{in}} ∪ y(t)|_{Ū_{i}∩C^{io}})
= ⋃_{i=1}^{n} g_{i}(r_{i}(t), (sŪ(t) ∪ y(t))|Ū_{i})
= ⋃_{i=1}^{n} g_{i}(r_{i}(t), (sŪ(t) ∪ ŷ(r(t), sŪ(t)))|Ū_{i})
= g(r(t), sŪ(t)).

For proving claim 3, we do a case distinction to separate the different cases in the definition of ẑ. Let t ∈ ℝ_{>0}.

Case A: r(t^{−}) = r(t) and sV̄(t) = 0. By well-behavedness (output triggering) of D, we have h(r(t^{−}), r(t), sV̄(t)) = 0. By construction of z and since z(t^{−}) = z(t), we have sZ̄(t) = 0. This implies sZ̄(t) = h(r(t^{−}), r(t), sV̄(t)).

Case B: r(t^{−}) ≠ r(t) or sV̄(t) ≠ 0. We prove claim 3 similarly as claim 2: By construction of z, we have z(t) = sZ̄(t)|_{E^{io}}. Furthermore, we have z(t) ∈ H(r̄(t^{−}), r̄(t), sV̄(t)), since for all i ∈ {1, …, n} the solution property holds for z(t):

h_{i}(r_{i}(t^{−}), r_{i}(t), (sV̄(t) ∪ z(t))|_{Z̄_{i}∩E^{io}})|_{Z̄_{i}∩E^{io}}
= h_{i}(r_{i}(t^{−}), r_{i}(t), (sV̄(t) ∪ sZ̄(t)|_{E^{io}})|_{Z̄_{i}∩E^{io}})|_{Z̄_{i}∩E^{io}}
= h_{i}(r_{i}(t^{−}), r_{i}(t), sV̄_{i}(t))|_{Z̄_{i}∩E^{io}}
= sZ̄_{i}(t)|_{Z̄_{i}∩E^{io}} = sZ̄(t)|_{Z̄_{i}∩E^{io}} = z(t)|_{Z̄_{i}∩E^{io}}.

So ẑ(r(t^{−}), r(t), sZ̄(t)) = z(t), yielding

sZ̄(t) = ⋃_{i=1}^{n} sZ̄_{i}(t) = ⋃_{i=1}^{n} h_{i}(r_{i}(t^{−}), r_{i}(t), sV̄_{i}(t))
= ⋃_{i=1}^{n} h_{i}(r_{i}(t^{−}), r_{i}(t), (sV̄(t) ∪ sZ̄(t))|V̄_{i})
= ⋃_{i=1}^{n} h_{i}(r_{i}(t^{−}), r_{i}(t), sV̄(t)|_{V̄_{i}∩E^{in}} ∪ sZ̄(t)|_{V̄_{i}∩E^{io}})
= ⋃_{i=1}^{n} h_{i}(r_{i}(t^{−}), r_{i}(t), sV̄(t)|_{V̄_{i}∩E^{in}} ∪ z(t)|_{V̄_{i}∩E^{io}})
= ⋃_{i=1}^{n} h_{i}(r_{i}(t^{−}), r_{i}(t), (sV̄(t) ∪ z(t))|V̄_{i})
= ⋃_{i=1}^{n} h_{i}(r_{i}(t^{−}), r_{i}(t), (sV̄(t) ∪ ẑ(r_{i}(t^{−}), r(t), sV̄(t)))|V̄_{i})
= h(r(t^{−}), r(t), sV̄(t)).

Finally, claim 1 holds: Since claims 2 and 3 hold, we have for all t ∈ ℝ_{>0}:

r(t)_{i} = r_{i}(t)
∈ f_{i}(r_{i}(t^{−}), sŪ_{i}(t^{−}), sV̄_{i}(t))
= f_{i}(r_{i}(t^{−}), (sŪ(t^{−}) ∪ sȲ(t^{−}))|Ū_{i}, (sV̄(t) ∪ sZ̄(t))|V̄_{i})
= f_{i}(r_{i}(t^{−}), \begin{matrix}(sŪ(t^{−}) ∪ g(r(t^{−}), sŪ(t^{−})))|Ū_{i}, \\ (sV̄(t) ∪ h(r(t^{−}), r(t), sV̄(t)))|V̄_{i}) \end{matrix}

= f(r(t^{−}), sŪ(t^{−}), sV̄(t))_{i},

for i ∈ {1, …, n}, and

r(t)_{n+1} = y(t) ∈ Σ_{C^{io}} = f(r(t^{−}), sŪ(t^{−}), sV̄(t))_{n+1},

r(t)_{n+2} = z(t) ∈ Σ_{E^{io}} = f(r(t^{−}), sŪ(t^{−}), sV̄(t))_{n+2}.

So r is a run of D over (sŪ, sV̄, sȲ, sZ̄). Thus, (sŪ, sV̄, sȲ, sZ̄) ∈ S_{D}. Condition 2 of Definition 4.10 has been proven, so S_{D} is a parallel interconnection of S_{D_{1}}, …, S_{D_{n}}.

Definition 4.28 (Discrete parallel interconnection with multiple solutions) Let {D_{1}, …, D_{n}} be consistent, and let the multiple solution property of Theorem 4.27 hold. The named DCES D gained from the construction above is called the discrete parallel interconnection with multiple solutions of D_{1}, …, D_{n}, denoted by D_{1} ||| … ||| D_{n}. □

Remark 4.29 To reduce the number of states and transitions in the resulting DCES in the construction above, one can

• reduce the states to those with y ∈ ⋃_{u∈Σ_{C^{in}}} G(x̄, u) since these y are the only possible choices for a condition output evaluation in that state (this can be done for z in a similar way), and

• reduce the set of initial states X_{0} to states with z = 0, since z is only used to make a nondeterministic choice of the event output evaluation when entering a state (however, this reduces neither the state space X nor the number of transitions).

We do not apply these reductions, since they make the proof of Theorem 4.27 harder to write and to read. For the implementation, however, if we aim towards model checking, space reduction might become vital. ◇

We conclude this chapter by giving an example for a discrete parallel interconnection having multiple solutions.

Example 4.30 Reconsider case 3 of Example 4.14. We have two interconnected DCES D_{1} and D_{2}. For i ∈ {1, 2}, we have the named DCES D_{i} = ({U_{i}}, ∅, {x}, {Y_{i}}, ∅, f_{i}, g_{i}, h_{i}, {x}) with α(U_{i}) = α(Y_{i}) = {a, b}, and, for all u ∈ Σ_{U_{i}},

• f_{i}(x, u, ∅) = {x},

• g_{i}(x, u)(Y_{i}) = u(U_{i}), and

• h_{i}(x, x, ∅) = ∅.

As formal semantics of D_{i}, we have the CES S_{D_{i}} = ({U_{i}}, ∅, {Y_{i}}, ∅, S_{D_{i}}) with

S_{D_{i}} = \begin{cases}(s_{U_{i}}, ∅, s_{Y_{i}}, ∅) ∈ Beh(\{U_{i}\}, ∅, \{Y_{i}\}, ∅) | \\ ∀t ∈ ℝ_{≥0} : s_{U_{i}}(t)(U_{i}) = s_{Y_{i}}(t)(Y_{i})\}, \end{cases}

for i ∈ {1, 2}. In both systems, the condition output symbol equals the condition input symbol at every moment.

D_{1}^{a ↦ a}^{b ↦ b}  ^{\overline{}}^{Y_{1}}^{U_{1}} D_{2}^{a ↦ a}^{b ↦ b}^{\overline{}}^{U_{2}}^{Y_{2}}

Figure 4.6: A parallel interconnection of DCESs with multiple solutions

The connections between D_{1} and D_{2} are characterized by U_{1} = Y_{2} ≠ Y_{1} = U_{2}, leading to the block diagram shown in Figure 4.6. We have no external inputs, so C^{in} = E^{in} = ∅. Furthermore, we have C^{io} = C^{out} = {U_{1}, U_{2}} and E^{io} = E^{out} = ∅.

Checking the multiple solution property of Theorem 4.27, we get the solution sets G((x, x), ∅) = {{U_{1} ↦ a, U_{2} ↦ a}, {U_{1} ↦ b, U_{2} ↦ b}} and H((x, x), (x, x), ∅) = {∅}. Now we use Definition 4.28 and construct the discrete parallel interconnection D = D_{1} ||| D_{2}. In the construction, we have to fix one element of each solution sets; we take pick(G((x, x), ∅)) = {U_{1} ↦ a, U_{2} ↦ a} and pick(H((x, x), (x, x), ∅)) = ∅.

We get the DCES D = (∅, ∅, X, {U_{1}, U_{2}}, ∅, f, g, h, X_{0}) with

• X = X_{0} = {x} × {x} × Σ_{{U_{1},U_{2}}} × Σ_{∅} = {(x, x, {U_{1} ↦ y_{1}, U_{2} ↦ y_{2}}, ∅) | y_{1}, y_{2} ∈ {a, b}},

• f(x̄, ∅, ∅) = X for all x̄ ∈ X,

• g((x, x, u, ∅), ∅) = \begin{cases}\{U_{1} ↦ a, U_{2} ↦ a\}, if u = & \{U_{1} ↦ a, U_{2} ↦ a\} \\ \{U_{1} ↦ b, U_{2} ↦ b\}, if u = & \{U_{1} ↦ b, U_{2} ↦ b\} \\ \{U_{1} ↦ a, U_{2} ↦ a\}, if u = & \{U_{1} ↦ a, U_{2} ↦ b\} \\ \{U_{1} ↦ a, U_{2} ↦ a\}, if u = & \{U_{1} ↦ b, U_{2} ↦ a\} \end{cases}, and

• h(x̄, x̄′, ∅) = ∅ for all x̄, x̄′ ∈ X.

Figure 4.7 shows a block diagram of D. There are four control states which can change arbitrarily; in one state the condition output {U_{1} ↦ b, U_{2} ↦ b} is generated, and {U_{1} ↦ a, U_{2} ↦ a} in the other three states.

[figure: D; U_{1}; U_{2}]
Figure 4.7: Block diagram of D = D_{1} ||| D_{2}

As semantics of the DCES D, we get the CES S_{D} = (∅, ∅, {U_{1}, U_{2}}, ∅, S_{D}) with

S_{D} = \begin{cases}(∅, ∅, s_{\{U_{1},U_{2}\}}, ∅) ∈ Beh(∅, ∅, \{U_{1}, U_{2}\}, ∅) | \\ ∀t ∈ ℝ_{≥0} : s_{\{U_{1},U_{2}\}}(t)(U_{1}) = s_{\{U_{1},U_{2}\}}(t)(U_{2})\}, \end{cases}

i.e., the two output condition symbols of S_{D} may change arbitrarily (in a finite-variable fashion), but they have to be equal in each time point. This is the behavior we expect from a parallel interconnection of S_{D_{1}} and S_{D_{1}} (see Definition 4.10, condition 2). ◇ 78

Introducing Quantitative Timing

As we have already seen in Example 2.8, the DCES model lacks a possibility of measuring time. This is, however, very important for process control models, where the desired properties of systems often include time constraints.

We could of course use CESs as a model for such purposes, but they cannot be described conveniently in a finite, operational way like DCESs. This fact makes CESs far too abstract, whereas DCESs can easily be implemented due to their operational structure. So it is straightforward to augment DCESs with timing features in such a way that the operational structure is preserved.

This is done by connecting a set of CESs to the DCES. These CESs are able to measure time and transfer timing information to the DCES. The DCES then can use this information to perform time-dependent actions. A CESs which is used for delivering timing information is defined as the semantics of a timer, which we introduce next.

5.1 Timers

To add quantitative timing to discrete condition/event systems, we introduce the notion of timers. A timer T is characterized by a list of positive integers which serve as thresholds for a real-valued clock. The timer value starts with 0 and increases at the same speed as the global time. The timer can be reset to 0 by sending a reset event to the timer. Besides this reset input (named Res_{T}), a timer has two output components, a condition component (named Int_{T}) which states in which interval between the thresholds the timer value is, and an event component (named Ala_{T}) which outputs an event if the timer value is exactly one of the thresholds.

Definition 5.1 (Timer) Let 𝕋 be a global set of identifiers. Any T ∈ 𝕋 is called timer. To each timer T we associate a nonempty, finite list Θ(T) = (θ_{T}^{1} , …, θ_{T}^{n_{T}}) of strictly increasing positive integers, called thresholds, and the following names and alphabets:

• interval condition name Int_{T} with alphabet α(Int_{T}) = {Int_{0}, …, Int_{n_{T}} },

• alarm event name Ala_{T} with alphabet α(Ala_{T}) = {0, Ala_{1}, …, Ala_{n_{T}} },

• reset event name Res_{T} with alphabet α(Res_{T}) = {0, Res}.

All condition and event symbols are considered to be different. For all T_{1}, T_{2} ∈ 𝕋 with T_{1} ≠ T_{2}, we demand {Int_{T_{1}}, Ala_{T_{1}}, Res_{T_{1}}} ∩ {Int_{T_{2}}, Ala_{T_{2}}, Res_{T_{2}}} = ∅, i.e., each timer has its own, unique component names. □

We define a timer function which measures the amount of time passed since the last occurrence of any proper event in a given signal. This signal will be the reset signal for the timer. Figure 5.1 shows the timer function where the only reset events are at t_{1}, t_{2}, and t_{3}.

[figure: t; τ(s_{v})(t); 0; 0; t_{1}; t_{2}; t_{3}]

Figure 5.1: Example of a timer function

Definition 5.2 (Timer function) Let s_{v} be any event signal. The timer function τ(s_{v}) : ℝ_{≥0} → ℝ_{≥0} with reset input signal s_{v} is defined by

τ(s_{v})(t) = t − max ({0} ∪ {t_{0} ∈ [0, t) | s_{v}(t_{0}) ≠ 0})

for all t ∈ ℝ_{≥0}. □

Note that if there is a proper event at time t in s_{v}, τ(s_{v})(t) delivers the “old” timer value, and τ(s_{v})(t + ε) = ε for all ε > 0 up to the next proper event (cf. Figure 5.1).

Now we can define the semantics of a timer T, which is done by associating a condition/event system S_{T} with T.

The behavior of S_{T} is as follows: Its event input is the reset signal for the clock of T; whenever S_{T} receives a proper event (which is Res), the clock is reset to 0. This is modeled by the timer function τ.

The output condition of S_{T} states in which interval between the timer’s thresholds the current timer value is. If the timer value is smaller than its first threshold θ_{T}^{1} or if the timer is receiving a reset event, the output condition symbol of S_{T} is Int_{0}. If the timer value is greater or equal than the last threshold θ_{T}^{n_{T}}, this is denoted by the condition symbol Int_{n_{T}}. And if the value of the timer is between θ_{T}^{i} and θ_{T}^{i+1}, S_{T} delivers the condition symbol Int_{i}.

The output event of S_{T} states if the timer value is exactly one of the thresholds. Whenever a threshold θ_{T}^{i} is reached, the alarm event Ala_{i} is generated. In all other cases, the output event of S_{T} is the null symbol. Note that if a reset event occurs exactly at the time when a threshold is reached, S_{T} also generates the alarm event for that threshold. Furthermore note that there is no Ala_{0} event.

S_{T} has no condition input components, so its set of condition input names is empty.

Definition 5.3 (Semantics of a timer) For a timer T ∈ 𝕋 the semantics of T is given by the condition/event system S_{T} = (∅, {Res_{T} }, {Int_{T} }, {Ala_{T} }, S_{T}) with S_{T} defined by (∅, s_{v}, s_{y}, s_{z}) ∈ S_{T} if and only if for every t ∈ ℝ_{≥0} we have

• s_{y}(t)(Int_{T}) = \begin{cases}Int_{0} , if & s_{v}(t) ≠ 0 & or & τ(s_{v})(t) < θ_{T}^{1} \\ Int_{i} , if & s_{v}(t) = 0 & and & τ(s_{v})(t) ∈ [θ_{T}^{i} , θ_{T}^{i+1}) \\ Int_{n_{T}}, if & s_{v}(t) = 0 & and & τ(s_{v})(t) ≥ θ_{T}^{n_{T}} \end{cases} and

• s_{z}(t)(Ala_{T}) = \begin{cases}Ala_{i}, if & τ(s_{v})(t) = θ_{T}^{i} \\ 0 , if & τ(s_{v})(t) ≠ θ_{T}^{i} for all i ∈ \{1, …, n_{T} \} \end{cases}

for all (∅, s_{v}, s_{y}, s_{z}) ∈ Beh(∅, {Res_{T} }, {Int_{T} }, {Ala_{T} }). □

The following lemma states that timers are really something new; we cannot express them by using a DCES.

Lemma 5.4 For any timer T ∈ 𝕋, there is no DCES D with S_{D} = S_{T}. □

Proof Let T ∈ 𝕋, and assume that we have a DCES D = (∅, {Res_{T} }, X, {Int_{T} }, {Ala_{T} }, f, g, h, X_{0}) with S_{D} = S_{T}. We construct a run of D over a behavior s. Let s_{Res_{T}} ∈ E({Res_{T} }), s_{Int_{T}} C({Int_{T} }), and s_{Ala_{T}} ∈ E({Ala_{T} }) such that for all t ∈ ℝ_{≥0}, s_{Res_{T}} (t) = 0, s_{Int_{T}} (t) = g(x_{0}, ∅), and s_{Ala_{T}} (t) = 0.

Obviously, we have s = (∅, s_{Res_{T}} , s_{Int_{T}} , s_{Ala_{T}}) ∈ Beh(∅, {Res_{T} }, {Int_{T} }, {Ala_{T} }). Let x_{0} ∈ X_{0}, and define r : ℝ_{≥0} → X by r(t) = x_{0} for all t ∈ ℝ_{≥0}.

We show that r is run of D over s: Since we have defined s_{Res_{T}} in such a way that there are no proper input events, stuttering allows D to stay always in the same state x_{0}, and by output triggering, there are no proper output events. And s_{Int_{T}} directly matches Definition 4.6. So r is a run of D over s, and therefore, s ∈ S_{D}.

Now we show that s ∉ S_{T}. Since there are no proper input events, Definition 5.2 yields τ(s_{Res_{T}})(t) = t for all t ∈ ℝ_{≥0}. So by Definition 5.3, we expect an alarm event at the first threshold of T: s_{Ala_{T}} (θ_{T}^{1} )(Ala_{T}) = Ala_{1}. This does not hold, so s ∉ S_{T}. Thus, S_{D} ≠ S_{T} and S_{D} ≠ S_{T}, contradicting our assumption.

5.2 Timed Condition/Event Systems

A timed condition/event system is a discrete condition/event system which is augmented with a set of timers. The outputs of the timers are connected to the inputs of the discrete condition/event system and vice versa. The signals between the discrete system and the timers are considered to be internal and are therefore not observable outside the system.

Definition 5.5 (Timed condition/event system) A timed condition/ event system (TCES) T = (Ū, V̄, Ȳ, Z̄, T̄, D) consists of

• a finite set of external condition input names Ū,

• a finite set of external event input names V̄,

• a finite set of external condition output names Ȳ,

• a finite set of external event output names Z̄,

• a finite set of timers T̄ ⊆ 𝕋, and

• a discrete condition/event system D = (Ū^{+}, V̄^{+}, X, Ȳ, Z̄^{+}, f, g, h, X_{0}), where

– Ū^{+} = Ū ∪ ⋃_{T ∈T̄}{Int_{T} }, – V̄^{+} = V̄ ∪ ⋃_{T ∈T̄}{Ala_{T} }, and

– Z̄^{+} = Z̄ ∪ ⋃_{T ∈T̄}{Res_{T} }.

Furthermore, let all sets of names be disjoint. □

Figure 5.2 shows a block diagram of a timed condition/event system with timer set T̄ = {T_{1}, …, T_{m}}.

[figure: D; Ū; V̄; {Int_{T_{1}}, …, Int_{T_{m}}}; {Ala_{T_{1}}, …, Ala_{T_{m}}}; Ȳ; Z̄; {Res_{T_{1}}, …, Res_{T_{m}}}] [figure: T_{1}; Int_{T_{1}}; Ala_{T_{1}}; Res_{T_{1}}] ⋮ ⋮  ⋮  ⋮ [figure: T_{m}; Int_{T_{m}}; Ala_{T_{m}}; Res_{T_{m}}]

Figure 5.2: Block diagram of a timed condition/event system

Now we define the semantics of a TCES. This is done by combining the signals of the TCES’s discrete system with the signals of the TCES’s timers. The components which are shown as connected in Figure 5.2 must have the same signals in S_{D} and in S_{T_{1}}, …, S_{T_{m}}.

Definition 5.6 (Semantics of a TCES) Let T = (Ū, V̄, Ȳ, Z̄, T̄, D) be a timed condition/event system. The semantics of T is defined by the condition/event system S_{T} = (Ū, V̄, Ȳ, Z̄, S_{T}) with (sŪ, sV̄, sȲ, sZ̄) ∈ S_{T} if and only if there exist (∅, s_{v}^{T} , s_{y}^{T} , s_{z}^{T}) ∈ S_{T} for every T ∈ T̄ such that

(sŪ ∪ ⋃_{T ∈T̄} s_{y}^{T} , sV̄ ∪ ⋃_{T ∈T̄} s_{z}^{T} , sȲ, sZ̄ ∪ ⋃_{T ∈T̄} s_{v}^{T}) ∈ S_{D},

for all (sŪ, sV̄, sȲ, sZ̄) ∈ Beh(Ū, V̄, Ȳ, Z̄). □

Obviously, a TCES having no timers is semantically equivalent to the DCES contained in it.

Lemma 5.7 Let T = (Ū, V̄, Ȳ, Z̄, T̄, D) be a timed condition/event system with T̄ = ∅. Then we have S_{T} = S_{D}. □

Another interesting but not surprising observation is that this construction is a parallel interconnection of the TCES’s discrete part with its timers.

Lemma 5.8 In Definition 5.6, S_{T} is a parallel interconnection of S_{D} and all S_{T}, T ∈ T̄ (if we hide the reset outputs of S_{D} and the timers’ outputs).

□

Proof Let T = (Ū, V̄, Ȳ, Z̄, T̄, D) be a timed condition/event system with T̄ = {T_{1}, …, T_{m}}, |T̄| = m. Define n = m + 1, S_{n} = S_{D}, S_{n} = S_{D}, and, for i ∈ {1, …, n − 1}, S_{i} = S_{T_{i}}, S_{i} = S_{T_{i}}. We show that S_{T} = (Ū, V̄, Ȳ, Z̄, S_{T}) is a parallel interconnection of S_{1}, …, S_{n}, if we hide the reset outputs of S_{n} and all outputs of S_{1}, …, S_{n−1}.

If we modify condition 1 of Definition 4.10 in accordance with this hiding (by omitting all timer related names in the two output name equations), we get

Ū = (⋃_{i=1}^{n−1} ∅ ∪ (Ū ∪ ⋃_{i=1}^{n−1}{Int_{T_{i}}})) \ (⋃_{i=1}^{n−1}{Int_{T_{i}}} ∪ Ȳ) ,
V̄ = (⋃_{i=1}^{n−1}{Res_{T_{i}}} ∪ (V̄ ∪ ⋃_{i=1}^{n−1}{Ala_{T_{i}}})) \
(⋃_{i=1}^{n−1}{Ala_{T_{i}}} ∪ (Z̄ ∪ ⋃_{i=1}^{n−1}{Res_{T_{i}}})) ,
Ȳ = Ȳ, and
Z̄ = Z̄,

which obviously holds, since Ū ∩ Ȳ = ∅ and V̄ ∩ Z̄ = ∅.

Also condition 2 of Definition 4.10 needs a slight modification: In part (b), we restrict the output signals to the non-timer components, resulting in the equations

sȲ_{i}|_{Ȳ_{i}∩Ȳ} = sȲ|_{Ȳ_{i}∩Ȳ} and sZ̄_{i}|_{Z̄_{i}∩Z̄} = sZ̄|_{Z̄_{i}∩Z̄}.

For proving this modified condition 2, let (sŪ, sV̄, sȲ, sZ̄) ∈ Beh(Ū, V̄, Ȳ, Z̄). We have

(sŪ, sV̄, sȲ, sZ̄) ∈ S_{T}

if and only if (by Definition 5.6)

∃(∅, s_{v}^{T} , s_{y}^{T} , s_{z}^{T}) ∈ S_{T} (for every T ∈ T̄) :
(sŪ ∪ ⋃_{T ∈T̄} s_{y}^{T} , sV̄ ∪ ⋃_{T ∈T̄} s_{z}^{T} , sȲ, sZ̄ ∪ ⋃_{T ∈T̄} s_{v}^{T}) ∈ S_{D}

if and only if (we introduce existential quantification for the signals of S_{D} = S_{n} and use an index i ∈ {1, …, n − 1} for the timers’ signals)

∃(sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}) ∈ S_{i} (for every i ∈ {1, …, n}) :
sŪ_{n} = sŪ ∪ ⋃_{i=1}^{n−1} sȲ_{i}, sȲ_{n} = sȲ,
sV̄_{n} = sV̄ ∪ ⋃_{i=1}^{n−1} sZ̄_{i}, sZ̄_{n} = sZ̄ ∪ ⋃_{i=1}^{n−1} sV̄_{i}

if and only if (we split the signals of S_{n} into timer and non-timer components)

∃(sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}) ∈ S_{i} (for every i ∈ {1, …, n}) :
(a) sŪ_{n}|_{Ū_{n}∩Ȳ_{j}} = sȲ_{j}|_{Ū_{n}∩Ȳ_{j}} for j ∈ {1, …, n − 1},
sV̄_{n}|_{V̄_{n}∩Z̄_{j}} = sZ̄_{j}|_{V̄_{n}∩Z̄_{j}} for j ∈ {1, …, n − 1},
sZ̄_{n}|_{V̄_{i}∩Z̄_{n}} = sV̄_{i}|_{V̄_{i}∩Z̄_{n}} for i ∈ {1, …, n − 1}.
(b) sŪ_{n}|_{Ū_{n}∩Ū} = sŪ|_{Ū_{n}∩Ū}, sȲ_{n}|_{Ȳ_{n}∩Ȳ} = sȲ|_{Ȳ_{n}∩Ȳ},
sV̄_{n}|_{V̄_{n}∩V̄} = sV̄|_{V̄_{n}∩V̄}, sZ̄_{n}|_{Z̄_{n}∩Z̄} = sZ̄|_{Z̄_{n}∩Z̄}.

if and only if (all equations we add in this step have signals over the empty name set on both sides are therefore trivially valid)

∃(sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}) ∈ S_{i} (for every i ∈ {1, …, n}) :

(a) For all i, j ∈ {1, …, n}:
sŪ_{i}|_{Ū_{i}∩Ȳ_{j}} = sȲ_{j}|_{Ū_{i}∩Ȳ_{j}},
sV̄_{i}|_{V̄_{i}∩Z̄_{j}} = sZ̄_{j}|_{V̄_{i}∩Z̄_{j}}.
(b) For all i ∈ {1, …, n}:
sŪ_{i}|_{Ū_{i}∩Ū} = sŪ|_{Ū_{i}∩Ū}, sȲ_{i}|_{Ȳ_{i}∩Ȳ} = sȲ|_{Ȳ_{i}∩Ȳ},
sV̄_{i}|_{V̄_{i}∩V̄} = sV̄|_{V̄_{i}∩V̄}, sZ̄_{i}|_{Z̄_{i}∩Z̄} = sZ̄|_{Z̄_{i}∩Z̄}.

We give a small example for a timed condition/event system.

Example 5.9 Recall Example 2.8 on page 21. We presented a CES S that generates a “ping” event at any time t ∈ ℕ \ {0}. Now we present a TCES T with S_{T} = S (since we did not have names in Chapter 2, a simple conversion is necessary). One timer with a single threshold 1 is needed in T . Every time the Ala_{1} event is received from the timer, the DCES part D of T generates the “ping” as an output event and resets the timer by sending the Res event.

Let T ∈ 𝕋 with Θ(T) = (1). Define T = ({U}, {V}, {Y}, {Z}, {T }, D) with α(U) = α(Y) = {0}, α(V) = {0}, α(Z) = {0, ping}, and D = (Ū^{+}, V̄^{+}, {x}, {Y}, Z̄^{+}, f, g, h, {x}), where (recall that g and h are functions mapping condition/event names to condition/event symbols)

• Ū^{+} = {U, Int_{T} }, V̄^{+} = {V, Ala_{T} }, Z̄^{+} = {Z, Res_{T} },

• f(x, u, v) = {x} for all u ∈ ΣŪ^{+}, v ∈ ΣV̄^{+},

• g(x, u) = {Y ↦ 0} for all u ∈ ΣŪ^{+}, and

• h(x, x, v) = \begin{cases}\{Z ↦ ping & , Res_{T} ↦ Res & \}, if v(Ala_{T}) = Ala_{1} \\ \{Z ↦ 0 & , Res_{T} ↦ 0 & \}, otherwise \end{cases} .

With these definitions, we have the expected behavior S_{T} = S. ◇

5.3 The Parallel Interconnection of Timed C/E Systems

Before we can reason about a parallel operator for timed condition/event systems, we define what consistency means for such systems. In addition to consistency for CESs and DCESs, we have to ensure that each discrete system uses its own set of timers; no sharing of timers is allowed.

Definition 5.10 (Consistent set of TCESs) For i ∈ {1, …, n}, let T_{i} = (Ū_{i}, V̄_{i}, Ȳ_{i}, Z̄_{i}, T̄_{i}, D_{i}) be a TCES. The set {T_{1}, …, T_{n}} is called consistent, if

(Ȳ_{i} ∪ Z̄_{i}) ∩ (Ȳ_{j} ∪ Z̄_{j}) = ∅ and T̄_{i} ∩ T̄_{j} = ∅

for all i, j ∈ {1, …, n} with i ≠ j. □

The parallel interconnection of TCESs can be constructed using the techniques presented in Chapter 4. We simply apply the discrete parallel interconnection to the DCESs inside the TCESs, getting a new DCES which serves as the discrete part of the TCES representing the composed system.

Theorem 5.11 Let T_{i} = (Ū_{i}, V̄_{i}, Ȳ_{i}, Z̄_{i}, T̄_{i}, D_{i}) be a TCES with D_{i} = (Ū_{i}^{+}, V̄_{i}^{+}, X_{i}, Ȳ_{i}, Z̄_{i}^{+}, f_{i}, g_{i}, h_{i}, X_{0,i}), for i ∈ {1, …, n}. Let {T_{1}, …, T_{n}} be consistent. A TCES T can be effectively constructed such that S_{T} is a parallel interconnection of S_{T_{1}}, …, S_{T_{n}}, if the multiple solution property of Theorem 4.27 holds for D_{1}, …, D_{n}. □

The discrete part that has to be constructed for T is just the discrete parallel interconnection (with multiple solutions) of D_{1}, …, D_{n}.

Proof Let T_{i} and D_{i}, i ∈ {1, …, n}, be given as in Theorem 5.11. Let the multiple solution property hold. Since {T_{1}, …, T_{n}} is consistent, {D_{1}, …, D_{n}} is also consistent, and by Theorem 4.27 we can define

D = (Ū^{+}, V̄^{+}, X, Ȳ, Z̄^{+}, f, g, h, X_{0}) = D_{1} ||| … ||| D_{n}.

Since {T_{1}, …, T_{n}} is consistent, we have no interference of the timer names, leading to

• Ū^{+} = ((⋃_{i=1}^{n} Ū_{i}) \ (⋃_{i=1}^{n} Ȳ_{i})) ∪ ⋃_{i=1}^{n} ⋃_{T ∈T̄_{i}}{Int_{T} },

• V̄^{+} = ((⋃_{i=1}^{n} V̄_{i}) \ (⋃_{i=1}^{n} Z̄_{i})) ∪ ⋃_{i=1}^{n} ⋃_{T ∈T̄_{i}}{Ala_{T} },

• Ȳ = ⋃_{i=1}^{n} Ȳ_{i}, and

• Z̄^{+} = (⋃_{i=1}^{n} Z̄_{i}) ∪ ⋃_{i=1}^{n} ⋃_{T ∈T̄_{i}}{Res_{T} }.

Now we define the TCES T = (Ū, V̄, Ȳ, Z̄, T̄, D) with

• Ū = (⋃_{i=1}^{n} Ū_{i}) \ (⋃_{i=1}^{n} Ȳ_{i}),

• V̄ = (⋃_{i=1}^{n} V̄_{i}) \ (⋃_{i=1}^{n} Z̄_{i}),

• Z̄ = ⋃_{i=1}^{n} Z̄_{i}, and

• T̄ = ⋃_{i=1}^{n} T̄_{i}.

Now we show that S_{T} is a parallel interconnection of S_{T_{1}}, …, S_{T_{n}}. Condition 1 of Definition 4.10 is obviously fulfilled. For proving condition 2, let (sŪ, sV̄, sȲ, sZ̄) ∈ Beh(Ū, V̄, Ȳ, Z̄). We have

(sŪ, sV̄, sȲ, sZ̄) ∈ S_{T}

if and only if (by Definition 5.6)

∃(∅, s_{v}^{T} s_{y}^{T} , s_{z}^{T}) ∈ S_{T} (for all T ∈ T̄) :
(sŪ ∪ ⋃_{T ∈T̄} s_{y}^{T} , sV̄ ∪ ⋃_{T ∈T̄} s_{z}^{T} , sȲ, sZ̄ ∪ ⋃_{T ∈T̄} s_{v}^{T}) ∈ S_{D}

if and only if (since S_{D} is a parallel interconnection of S_{D_{1}}, …, S_{D_{n}}, we can use Definition 4.10)

∃(∅, s_{v}^{T} s_{y}^{T} , s_{z}^{T}) ∈ S_{T} (for all T ∈ T̄) :
∃(sŪ_{i}^{+}, sV̄_{i}^{+}, sȲ_{i}, sZ̄_{i}^{+}) ∈ S_{D_{i}} (for all i ∈ {1, …, n}) :
(a) For all i, j ∈ {1, …, n}:
sŪ_{i}^{+}|_{Ū_{i}^{+}∩Ȳ_{j}} = sȲ_{j}|_{Ū_{i}^{+}∩Ȳ_{j}}, sV̄_{i}^{+}|_{V̄_{i}^{+}∩Z̄_{j}^{+}} = sZ̄_{j}^{+}|_{V̄_{i}^{+}∩Z̄_{j}^{+}}.
(b) For all i ∈ {1, …, n}:
sŪ_{i}^{+}|_{Ū_{i}^{+}∩Ū^{+}} = (sŪ ∪ ⋃_{T ∈T̄} s_{y}^{T})|_{Ū_{i}^{+}∩Ū^{+}}, sȲ_{i} = sȲ|Ȳ_{i},
sV̄_{i}^{+}|_{V̄_{i}^{+}∩V̄^{+}} = (sV̄ ∪ ⋃_{T ∈T̄} s_{z}^{T})|_{V̄_{i}^{+}∩V̄^{+}}, sZ̄_{i}^{+} = (sZ̄ ∪ ⋃_{T ∈T̄} s_{v}^{T})|Z̄_{i}.

if and only if (we split the signals of the S_{D_{i}} into their non-timer and timer parts)

∃(∅, s_{v}^{T} s_{y}^{T} , s_{z}^{T}) ∈ S_{T} (for all T ∈ T̄) : ∃sŪ_{i} ∈ ΣŪ_{i}, sV̄_{i} ∈ ΣV̄_{i}, sȲ_{i} ∈ ΣȲ_{i}, sZ̄_{i} ∈ ΣZ̄_{i}, ∃s_{u_{i}}^{T} ∈ Σ_{Ū_{i}^{+}\Ū_{i}}, s_{v_{i}}^{T} ∈ Σ_{V̄_{i}^{+}\V̄_{i}}, s_{z_{i}}^{T} ∈ Σ_{Z̄_{i}^{+}\Z̄_{i}} with (sŪ_{i} ∪ s_{u_{i}}^{T}, sV̄_{i} ∪ s_{v_{i}}^{T}, sȲ_{i}, sZ̄_{i} ∪ s_{z_{i}}^{T}) ∈ S_{D_{i}} (for all i ∈ {1, …, n}) :

(a) For all i, j ∈ {1, …, n}:

sŪ_{i}|_{Ū_{i}∩Ȳ_{j}} = sȲ_{j}|_{Ū_{i}∩Ȳ_{j}}, sV̄_{i}|_{V̄_{i}∩Z̄_{j}} = sZ̄_{j}|_{V̄_{i}∩Z̄_{j}}.

(b) For all i ∈ {1, …, n}:

sŪ_{i}|_{Ū_{i}∩Ū} = sŪ|_{Ū_{i}∩Ū}, s_{u_{i}}^{T} = ⋃_{T ∈T̄_{i}} s_{y}^{T} , sV̄_{i}|_{V̄_{i}∩V̄} = sV̄|_{V̄_{i}∩V̄}, s_{v_{i}}^{T} = ⋃_{T ∈T̄_{i}} s_{z}^{T} , sȲ_{i} = sȲ|Ȳ_{i}, sZ̄_{i}|_{Z̄_{i}∩Z̄} = sZ̄|_{Z̄_{i}∩Z̄}, s_{z_{i}}^{T} = ⋃_{T ∈T̄_{i}} s_{v}^{T} .

if and only if (some existentially quantified timer signals are completely fixed by others; we replace s_{u_{i}}^{T} by ⋃_{T ∈T̄_{i}} s_{y}^{T}, s_{v_{i}}^{T} by ⋃_{T ∈T̄_{i}} s_{z}^{T}, and s_{z_{i}}^{T} by ⋃_{T ∈T̄_{i}} s_{v}^{T}, for all i ∈ {1, …, n})

∃(∅, s_{v}^{T} , s_{y}^{T} , s_{z}^{T}) ∈ S_{T} (for all T ∈ T̄_{i}) : ∃sŪ_{i} ∈ ΣŪ_{i}, sV̄_{i} ∈ ΣV̄_{i}, sȲ_{i} ∈ ΣȲ_{i}, sZ̄_{i} ∈ ΣZ̄_{i} with (sŪ_{i} ∪ ⋃_{T ∈T̄_{i}} s_{y}^{T} , sV̄_{i} ∪ ⋃_{T ∈T̄_{i}} s_{z}^{T} , sȲ_{i}, sZ̄_{i} ∪ ⋃_{T ∈T̄_{i}} s_{v}^{T}) ∈ S_{D_{i}} (for all i ∈ {1, …, n}) :

(a) For all i, j ∈ {1, …, n}:

sŪ_{i}|_{Ū_{i}∩Ȳ_{j}} = sȲ_{j}|_{Ū_{i}∩Ȳ_{j}}, sV̄_{i}|_{V̄_{i}∩Z̄_{j}} = sZ̄_{j}|_{V̄_{i}∩Z̄_{j}}.

(b) For all i ∈ {1, …, n}:

sŪ_{i}|_{Ū_{i}∩Ū} = sŪ|_{Ū_{i}∩Ū}, sȲ_{i} = sȲ|Ȳ_{i}, sV̄_{i}|_{V̄_{i}∩V̄} = sV̄|_{V̄_{i}∩V̄}, sZ̄_{i} = sZ̄|Z̄_{i}.

if and only if (by Definition 5.6)

∃(sŪ_{i}, sV̄_{i}, sȲ_{i}, sZ̄_{i}) ∈ S_{T_{i}} (for all i ∈ {1, …, n}) :

(a) For all i, j ∈ {1, …, n}:

sŪ_{i}|_{Ū_{i}∩Ȳ_{j}} = sȲ_{j}|_{Ū_{i}∩Ȳ_{j}}, sV̄_{i}|_{V̄_{i}∩Z̄_{j}} = sZ̄_{j}|_{V̄_{i}∩Z̄_{j}}.

(b) For all i ∈ {1, …, n}:

sŪ_{i}|_{Ū_{i}∩Ū} = sŪ|_{Ū_{i}∩Ū}, sȲ_{i} = sȲ|Ȳ_{i}, sV̄_{i}|_{V̄_{i}∩V̄} = sV̄|_{V̄_{i}∩V̄}, sZ̄_{i} = sZ̄|Z̄_{i}.

Definition 5.12 (Discrete parallel interconnection of TCESs) Let the set {T_{1}, …, T_{n}} of timed condition/event systems be consistent, and let the multiple solution property of Theorem 4.27 hold. The TCES T gained from the construction above is called the discrete parallel interconnection of T_{1}, …, T_{n}, denoted by T_{1} ||| … ||| T_{n}. □

Remark 5.13 Theorem 5.11 and Definition 5.12 can also be formulated for unique solutions, based on Theorem 4.13 and Definition 4.15. Construction and proof are analogous. We denote the discrete parallel interconnection with unique solutions of some consistent TCESs T_{1}, …, T_{n} by T_{1}∥ … ∥T_{n}. ◇

Furthermore, since every DCES is expressible as a TCES (see Lemma 5.7), we also allow DCESs as parameters for the two parallel interconnection operators given above.

90

Example: The Evaporator System

The example we are about to give in this chapter is a part of an experimental batch plant used in the Process Control Laboratory at the Chemical Engineering Department, University of Dortmund. This plant is used to illustrate a chemical batch process, its operation, and its automated control. A description of the full plant can be found in [Kow95].

Figure 6.1 shows the part of the plant we are going to examine. It mainly consists of four physical devices: Two tanks in which liquids and steam can be kept, a condenser which is able to cool steam down to water, and a heating device for increasing the temperature of the liquid inside the first tank. There are one-way pipes between tank 1 and tank 2, tank 1 and the condenser, and there are pipes to fill tank 1, to empty tank 2, and to remove the water from the condenser. Some pipes can be opened or closed using valves.

The normal operation of this system part is a follows: Tank 1 is filled through valve 1 with a salt solution of low concentration. Then the heater is switched on, and the concentration of the solution rises, while steam evaporates from tank 1 into the condenser. If the condenser works properly, the steam cools down to water and leaves the condenser. When a certain concentration is reached, the heater is switched off, and tank 1 is emptied via valve 2 into tank 2. A postprocessing step takes place in tank 2, then the solution leaves this part of the system via valve 3.

6.1 The Problem

In our example, we are not interested in the normal operation, but on the system’s reaction to certain malfunctions which may endanger the safety of the plant. Consider the following scenario: During the evaporation of the solution in tank 1, the condenser malfunctions, for example due to missing

[figure: Condenser; Tank 1; Heater; Valve 1; Tank 2; Valve 2; Valve 3]

Figure 6.1: Diagram of the evaporator system

cooling agent. Hence, the steam cannot be cooled, and the pressure inside the condenser starts to rise. Now the heater in tank 1 has to be switched off to prevent further production of steam, since exceeding a certain pressure limit may cause the condenser to explode.

After having switched off the heater in the case of a condenser malfunction, another problem arises: If the temperature in tank 1 cools down below a certain temperature, the solution might get solid and cannot be drained into tank 2. Therefore, valve 2 must be opened early enough to let the solution flow into tank 2, where the postprocessing step prevents the solution from getting solid. However, before valve 2 can be opened, we must ensure that tank 2 is empty; otherwise an overflow occurs in tank 2. So we might have to open valve 3 first to drain tank 2.

Let us summarize the characteristics of a sensible strategy to react on a cooling malfunction in the condenser: The heater has to be switched off early enough to prevent an explosion of the condenser, but not too early, because the solution may become solid while we wait for tank 2 being emptied. To keep this time slot as large as possible, it seems to be reasonable to open valve 3 immediately if we detect a cooling malfunction and tank 2 is not empty.

Our task is now to model a controller which can cope with the problems discussed above. The controller, which can influence the system by switching off the heater and using valves 2 and 3 to drain both tanks, must fulfill the following safety properties:

1. If a cooling malfunction in the condenser occurs, the heater must be switched off fast enough such that the condenser does not explode.

2. If the heater is switched off, tank 1 is drained into tank 2 before the solution gets solid.

3. If valve 2 is opened to drain tank 1 into tank 2, tank 2 has to be empty.

We will give formalized versions of these properties after we have defined a formal model of the system with its controller.

The following timing parameters are given by the physical characteristics of the batch plant:

• If the condenser malfunctions and the production of steam in tank 1 continues, the condenser may explode after more than 8 time units.

• If the heater in tank 1 is switched off, it takes exactly 5 time units until the production of steam stops.

• If the production of steam stops in tank 1, the solution may get solid after more than 4 time units.

• It takes between 0 and 10 time units to empty tank 2.

The draining of tank 1 is supposed to be fast enough, so no timing constraint is given here.

6.2 The Model

The system consisting of the four physical devices and the controller is modeled by a parallel interconnection of timed condition/event systems, or, where no quantitative timing is needed, discrete condition/event systems. A block diagram of the complete system is given in Figure 6.2. All signals shown are event signals.

The evaporator system consists of six modules. The modules and their functions are:

[figure: Controller; Tank-1; Tank-2; Heater; Pressure; Condenser; Malfunction; Malfunction; Switch; Heat; Heat; Drain-1; Drain-1; Drain-2; Drain-2; Empty; Empty]

Figure 6.2: Block diagram of the evaporator system model

• Tank-1 models tank 1, including its contents and valve 2.

• Tank-2 models tank 2, including its contents and valve 3.

• Heater models the heater in tank 1.

• Condenser models the condenser.

• Pressure models the pressure in the condenser.

• Controller models the controller of the plant.

There exist several other possibilities for splitting up the system into modules; for example, one can model Condenser and Pressure as one module. The split chosen here is a tradeoff between a small number of modules and a low complexity of each module.

Before we define a TCES for each module, we take a look at the events used in the system. For each event name N in the system, we give the proper event in α(N), and we explain its meaning. Each of the alphabets has just one proper event.

• Malfunction: The event mal is generated by Condenser to indicate that it starts malfunctioning, i.e., the cooling of the steam no longer works.

• Switch: The event off is sent from Controller to Heater to indicate that the heating device should switch off.

• Heat: The event off from Heater indicates that the heating device has switched off and no steam is produced in tank 1 any longer.

• Drain-1: The event drain is sent from Controller to Tank-1 to open valve 2 and start draining the contents of tank 1 into tank 2.

• Drain-2: The event drain is sent from Controller to Tank-2 to open valve 3 and start draining tank 2.

• Empty: The event empty from Tank-2 indicates that the draining of tank 2 is completed, tank 2 is empty, and valve 3 has been closed.

Since we are only interested in the malfunction scenario, we do not model the evaporator system’s normal behavior, but only the parts that are involved in bringing the system to a safe state if a condenser malfunction occurs. Thus, we assume that all valves are closed, tank 1 has already been filled, the heater is switched on, and the condenser works properly. Furthermore, since we are interested in a worst case scenario, tank 2 is also filled initially.

6.2.1 The Modules

The modules of the evaporator system are specified as TCESs. In the module Condenser, no quantitative timing is needed, and thus, it is specified as a DCES. In addition to the connections shown in Figure 6.2, each module has one condition output component. The output symbol of this component is an abstraction of the current control state of the module. We will later use these symbols to verify the three properties mentioned before.

For every module, we give a block diagram showing its input and output components. To keep the diagrams simple, the timers and their connections are not shown. Furthermore, its discrete functions f, g, and h are given, using a graphical representation which is explained in detail in the definition of Tank-1 .

6.2.1.1 The TCES Tank-1

Figure 6.3 shows the block diagram of the TCES Tank-1 . Tank-1 works as follows: Initially, tank 1 is full. If the drain event is received via component Drain-1 from Controller, tank 1 gets empty. If the off event is received via component Heat from Heater, the solution in tank 1 is in danger of getting solid. A timer with a single threshold of 4 is started, and after 4 time units, the solution may get solid. If the drainevent occurs within this period, tank 1 gets empty, and this part of the system is safe. If the drain event is sent after

Tank-1 [figure: Heat; Drain-1; StatusTank-1]

Figure 6.3: Block diagram of the TCES Tank-1

more than 4 time units, the solution might have become solid, or it might not. In this case it is not predictable if the system will get safe.

We define the TCES

Tank-1 = (∅, {Heat, Drain-1}, {StatusTank-1}, ∅, {T_{T 1}}, D_{Tank-1} )

with α(Heat) = {0, off}, α(Drain-1) = {0, drain}, α(StatusTank-1) = {full, danger, empty, solid}, Θ(T_{T 1}) = (4), and

D_{Tank-1} = (\begin{matrix}\{Int_{T_{T 1}}\}, \{Heat, Drain-1, Ala_{T_{T 1}}\}, \{x_{0}, x_{1}, x_{2}, x_{3}\}, \\ \{StatusTank-1\}, \{Res_{T_{T 1}}\}, f_{1}, g_{1}, h_{1}, \{x_{0}\}). \end{matrix}

The functions f_{1}, g_{1} and h_{1} are given by a graphical representation in Figure 6.4. The circles represent the control states; at the top of each circle

[figure: x_{3}; empty; x_{0}; full; x_{1}; danger; x_{2}; solid; Heat : off, Drain-1 : 0; /Res_{T_{T 1}} : Res; Int_{T_{T 1}} : Int_{1}; Heat : off, Drain-1 : 0; Drain-1 : drain; Drain-1 : drain]

Figure 6.4: Discrete part of the TCES Tank-1

the identifier x_{i} for that state is given. Since all condition output functions we define in this chapter are independent from the condition input symbols (there are only those sent from the timers), we just put the condition output symbol into each state. Thus, Figure 6.4 defines g_{1}(x_{0}, u)(StatusTank-1) = full, g_{1}(x_{1}, u)(StatusTank-1) = danger, g_{1}(x_{2}, u)(StatusTank-1) = solid, and g_{1}(x_{3}, u)(StatusTank-1) = empty, for all u ∈ Σ_{Int_{T_{T 1}}}. We will use these output condition symbols for verification purposes only.

The edges in Figure 6.4 define f_{1} and h_{1}. An edge from a state x_{i} to a state x_{j} denotes that there are u, v such that x_{j} ∈ f_{1}(x_{i}, u, v). The possible values for u and v are described by the labeling of that edge. For example, the edge from x_{0} to x_{1} defines the following state transitions:

For all u ∈ Σ_{Int_{T_{T 1}}}, v ∈ Σ_{{Heat,Drain-1,Ala_{T_{T 1}}}} :
x_{1} ∈ f_{1}(x_{0}, u, v) if v(Heat) = off ∧ v(Drain-1) = 0.

Everything after the slash (/) is used to indicate the event output evaluation generated by h_{1} during that transition. For example, the edge from x_{0} to x_{1} defines the following event output:

For all v ∈ Σ_{{Heat,Drain-1,Ala_{T_{T 1}}}} :
h_{1}(x_{0}, x_{1}, v)(Res_{T_{T 1}}) = Res if v(Heat) = off ∧ v(Drain-1) = 0.

Note that the parts of u and v not fixed in the labeling may have any value.

If for some x, u, and v there is no edge leaving state x having a labeling describing u and v, we assume f_{1}(x, u, v) = {x}, i.e., there is no state change in state x for the input evaluations u and v. Furthermore, we assume x ∈ f_{1}(x, u, 0) for any x and u to obtain stuttering. And if there is no edge from state x to x′ describing the event output evaluation of some name N for some event input evaluation v, we assume h_{1}(x, x′, v)(N) = 0, i.e., there is no proper event generated. With these default values, stuttering and output triggering can be checked easily.

Take again a look at Figure 6.4. The edge from x_{1} to x_{2} allows a transition leaving x_{1} at any time after timer T_{T 1} has reached its first (and only) threshold, which is 4. If the event drain arrives after this threshold has been reached, there two transitions possible: one to the “good” state x_{3}, and one to the “bad” state x_{2}. This nondeterminism models that after 4 time units, a draining command from the controller may arrive early enough, or it may not. To be on the safe side in any case, the last possibility to send drain must be exactly 4 time units after off was sent by Heater.

The self-loop edge from x_{1} to x_{1} is only used to prevent the forcing of the transition from x_{1} to x_{2} in case further Heat : off events occur at state x_{1}. Since the labeling on the edge from x_{1} to x_{2} does not contain the name Heat, there exists a transition from x_{1} to x_{2} which is triggered by Heat : off, and therefore the defaults for f_{1} described above will not implicitly assume the self-loop we defined explicitly.

6.2.1.2 The TCES Tank-2

Figure 6.5 shows the block diagram of the TCES Tank-2 . Tank-2 works as

Tank-2 [figure: Drain-1; Drain-2; Empty; StatusTank-2]

Figure 6.5: Block diagram of the TCES Tank-2

follows: Initially, tank 2 is full. If the drain event is received via component Drain-2 from Controller, tank 2 starts to drain. A clock is used to ensure that within 10 time units, the empty symbol is sent via component Empty to Controller, denoting that tank 2 is empty. If the drain event occurs while tank 2 is still full or in the process of draining, tank 2 overflows.

We define the TCES

Tank-2

= (∅, {Drain-1, Drain-2}, {StatusTank-2}, {Empty}, {T_{T 2}}, D_{Tank-2} )

with α(Drain-1) = {0, drain}, α(Drain-2) = {0, drain}, α(StatusTank-2) = {full, empty, draining, overflow}, α(Empty) = {0, empty}, Θ(T_{T 2}) = (10), and

D_{Tank-2} = (\begin{matrix}\{Int_{T_{T 2}}\}, \{Drain-1, Drain-2, Ala_{T_{T 2}}\}, \{x_{0}, x_{1}, x_{2}, x_{3}\}, \\ \{StatusTank-2\}, \{Empty, Res_{T_{T 2}}\}, f_{2}, g_{2}, h_{2}, \{x_{0}\}). \end{matrix}

The functions f_{2}, g_{2} and h_{2} are given by Figure 6.6. Note that there are two different kinds of transitions denoted by the edge from x_{2} to x_{1}; one state transition that may be taken within 10 time units, and one transition that must be taken when 10 time units have elapsed. The first transition is only enabled by the condition symbol Int_{0}, while the second one is forced by the event symbol Ala_{1}, because we have no transition from x_{2} to itself labeled with Ala_{T_{T 2}} : Ala_{1}. Since the occurrence of Ala_{1} is allowed for transitions from x_{2} to x_{1}, this is the only way to go. This models the fact that draining tank 2 may take up to 10 time units, but at time 10 tank 2 must be empty. Note however that draining tank 1 exactly 10 time units after draining tank 2 will lead to an overflow of tank 2. Any time later is safe in all cases.

The self-loop edge from x_{2} to x_{2} is only used to prevent the forcing of the transition from x_{2} to x_{1} in case further Drain-2 : drain events occur at state x_{1} before 10 time units have elapsed.

[figure: x_{0}; full; x_{1}; empty; x_{2}; draining; x_{3}; overflow; Drain-1 : 0, Drain-2 : drain; /Res_{T_{T 2}} : Res; Drain-1 : drain; Drain-1 : drain; Drain-1 : drain; Drain-1 : 0, ; Int_{T_{T 2}} : Int_{0}; /Empty : empty; Drain-1 : 0, Drain-2 : drain, Ala_{T_{T 2}} : 0]

Figure 6.6: Discrete part of the TCES Tank-2

6.2.1.3 The TCES Heater

Figure 6.7 shows the block diagram of the TCES Heater. Heater works as

Heater [figure: Switch; Heat; StatusHeater]

Figure 6.7: Block diagram of the TCES Heater

follows: Initially, the heater is working, and steam is produced in tank 1. If the off event is received via component Switch from Controller, the heater is switched off. Since it takes 5 time units for the heater to cool down such that no steam is produced any more, a timer is used to send the off event after 5 time units via component Heat to denote that no steam is produced any longer.

We define the TCES

Heater = (∅, {Switch}, {StatusHeater}, {Heat}, {T_{H}}, D_{Heater})

with α(Switch) = {0, off}, α(Heat) = {0, off}, α(StatusHeater) = {on, cold, cooling}, Θ(T_{H}) = (5), and

D_{Heater} = (\begin{matrix}\{Int_{T_{H}}\}, \{Switch, Ala_{T_{H}}\}, \{x_{0}, x_{1}, x_{2}\}, \\ \{StatusHeater\}, \{Heat, Res_{T_{H}}\}, f_{H}, g_{H}, h_{H}, \{x_{0}\}). \end{matrix}

The functions f_{H}, g_{H} and h_{H} are given by Figure 6.8. Note that unlike in Figure 6.6, where there is a transition that may be taken, the edge from x_{1} to x_{2} denotes that a transition must be taken if and only if the Ala_{1} event occurs. Hence, the off event in component Heat is always sent exactly 5 time units after off has been received via component Switch.

[figure: x_{0}; on; x_{1}; cooling; x_{2}; cold; Ala_{T_{H}} : Ala_{1}; /Heat : off; Switch : off; /Res_{T_{H}} : Res]

Figure 6.8: Discrete part of the TCES Heater

6.2.1.4 The DCES Condenser

Figure 6.9 shows the block diagram of the DCES Condenser. Since this

Condenser

\overline{}Malfunction

\overline{}StatusCondenser

Figure 6.9: Block diagram of the DCES Condenser

system needs no timers, is it modeled as a DCES. Condenser has two states; one showing that it is working, and one denoting that it is malfunctioning. Initially, the condenser is working. It can malfunction at any time by sending the mal event via component Malfunction.

[figure: x_{0}; normal]

[figure: x_{1}; fail]

/Malfunction : mal

Figure 6.10: Discrete part of the DCES Condenser

We have the DCES

Condenser = (\begin{matrix}∅, ∅, \{x_{0}, x_{1}, x_{2}\}, \{StatusCondenser\}, \{Malfunction\}, \\ f_{C}, g_{C}, h_{C}, \{x_{0}\}) \end{matrix} with α(Malfunction) = {0, mal} and α(StatusCondenser) = {normal, fail}. The functions f_{C}, g_{C} and h_{C} are given by Figure 6.10.

6.2.1.5 The TCES Pressure

Figure 6.11 shows the block diagram of the TCES Pressure. Pressure is

Pressure [figure: Malfunction; Heat; StatusPressure]

Figure 6.11: Block diagram of the TCES Pressure

used to model the pressure inside the condenser. Initially, we have normal pressure. If a malfunction of the condenser occurs, the event mal is received via component Malfunction, and we are in danger, since steam is still produced in tank 1. A timer is used to wait for 8 time units before the pressure may get too high and the condenser explodes. If the event off is received early enough from Heater via component Heat, the steam production has been stopped, and we are safe again.

[figure: x_{0}; normal; x_{1}; danger; x_{2}; too-high; Int_{T_{P}} : Int_{1}; Malfunction : mal, Heat : 0; Malfunction : mal, Heat : 0; /Res_{T_{P}} : Res; Heat : off]

Figure 6.12: Discrete part of the TCES Pressure

We define the TCES

Pressure = (∅, {Malfunction, Heat}, {StatusPressure}, ∅, {T_{P} }, D_{Pressure})

with α(Malfunction) = {0, mal}, α(Heat) = {0, off}, α(StatusPressure) = {normal, danger, too-high}, Θ(T_{P}) = (8), and

D_{Pressure} = (\begin{matrix}\{Int_{T_{P}} \}, \{Malfunction, Heat, Ala_{T_{P}} \}, \{x_{0}, x_{1}, x_{2}\}, \\ \{StatusPressure\}, \{Res_{T_{P}} \}, f_{P} , g_{P} , h_{P} , \{x_{0}\}). \end{matrix}

The functions f_{P}, g_{P} and h_{P} are given by Figure 6.12. In the unlike case the malfunction occurs and the heater stops producing steam at the same time, we are safe and stay in state x_{0}. Like in Figure 6.4, the transition from state x_{1} to x_{2} may be taken any time after timer T_{P} has reached its threshold, and the last safe possibility to receive off must be exactly 8 time units after mal was sent by Condenser.

Again, the self-loop edge from x_{1} to x_{1} is only used to prevent the forcing of the transition from x_{1} to x_{2} by further Malfunction : mal events.

6.2.1.6 The TCES Controller

Figure 6.13 shows the block diagram of the TCES Controller. It works as

Controller [figure: StatusController; Malfunction; Heat; Empty; Drain-1; Drain-2; Switch]

Figure 6.13: Block diagram of the TCES Controller

follows: When the event mal is received from Condenser, the event drain is sent via component Drain-2 to Tank-2 within 1 time unit, and tank 2 is drained. Then the heater is switched off by sending the event off via component Switch to Heater. This must happen more than 2 time units after drain was sent, and within 3 time units after mal was received. If the empty event arrives from Tank-2 earlier, off is sent immediately. Then we wait for the event off to arrive from Heater and empty to arrive from Tank-2 (if it has not been received yet). Exactly 4 time units after the empty event was received from Tank-2 , the drain event is sent to Tank-1 , tank 1 is emptied, and the system is safe.

We define the TCES

Controller = (\begin{matrix}∅, \{Malfunction, Heat, Empty\}, \{StatusController\}, \\ \{Drain-1, Drain-2, Switch\}, \{T_{1}, T_{2}\}, D_{Controller}) \end{matrix}

with α(Malfunction) = {0, mal}, α(Heat) = {0, off}, α(StatusController) = {normal, danger, safe}, α(Empty) = {0, empty}, Θ(T_{1}) = (1, 3, 4), Θ(T_{2}) = (2), and

D_{Controller} = (\begin{matrix}\{Int_{T_{1}}, Int_{T_{2}}\}, \{Malfunction, Heat, Empty, Ala_{T_{1}}, Ala_{T_{2}}\}, \\ \{x_{0}, x_{1}, x_{2}, x_{3}, x_{4}, x_{5}, x_{6}, x_{7}\}, \{StatusController\}, \\ \{Drain-1, Drain-2, Switch, Res_{T_{1}}, Res_{T_{2}}\}, f, g, h, \{x_{0}\}). \end{matrix}

6.2. The Model 103

[figure: x_{7}; safe]

[figure: x_{6}; danger]

[figure: x_{5}; danger]

[figure: x_{4}; danger]

[figure: x_{3}; danger]

[figure: x_{2}; danger]

[figure: x_{1}; danger]

[figure: x_{0}; normal]

Malfunction : mal /Res_{T_{1}} : Res

Int_{T_{1}} : Int_{0} /Drain-2 : drain, Res_{T_{2}} : Res

Empty : 0, ; Int_{T_{1}} : Int_{1}, ; Int_{T_{2}} : Int_{1} ; /Switch : off

Empty : empty /Switch : off

Empty : 0, ; Heat : off ; /Res_{T_{1}} : Res

\overline{}Empty : empty, Heat : 0

Heat : off ; /Res_{T_{1}} : Res

Empty : empty,

Heat : off /Res_{T_{1}} : Res

\overline{}Empty : empty

Ala_{T_{1}} : Ala_{3} /Drain-1 : drain

Figure 6.14: Discrete part of the TCES Controller The functions f, g and h are given by Figure 6.14. To keep the transition diagram simple, the following three self-loop edges are not drawn in Figure 6.14: One edge at state x_{1} with label “Ala_{T_{1}} : 0”, an edge at state x_{2} labeled with “Empty : 0, Ala_{T_{1}} : 0”, and another edge at x_{2} labeled with “Empty : 0, Ala_{T_{1}} : Ala_{1}”. These edges ensure that the transition from state x_{1} to x_{2} is forced only by the Ala_{1} event of timer T_{1}, and the transition from state x_{2} to x_{3} is forced only by the Ala_{2} event of timer T_{1}.

We take a look at the timing taking place in Controller. Two timers, T_{1} with threshold list (1, 3, 4) and T_{2} with a single threshold (2), are used. The transition from x_{0} to x_{1} resets timer T_{1}. Timer T_{1} is used to measure the time elapsed since event mal occurred. The transition from x_{1} to x_{2} is enabled only while the value of T_{1} is below T_{1}’s first threshold, which is 1. When the value of T_{1} is 1, the alarm event of T_{1} forces the transition from x_{1} to x_{2} to be taken, since we have no transition from x_{1} to itself labeled with Ala_{T_{1}} : Ala_{1}. During this transition, timer T_{2} is reset, and starts counting the time since the event drain was sent to Tank-2 .

In state x_{2}, we either wait for the event empty to be sent by Tank-2 , forcing us to go to state x_{4}, or we wait for a certain time to elapse before we go to state x_{3}. As said before, the point in time we are waiting for is at least 2 time units after drain was sent, and at most 3 time units after mal was received. Thus, both timer values have to be beyond their first threshold, denoted by the condition symbol Int_{1}. The edge from state x_{2} to state x_{3} enables the transition under these conditions. If the value of timer T_{1} reaches 3, we have to take the transition from x_{2} to x_{3}. This is forced by the event Ala_{2} generated by T_{1}. Since we have no edge from x_{2} to itself labeled with Ala_{T_{1}} : Ala_{2}, we cannot stay in state x_{2} and must go to state x_{3}.

In states x_{3} and x_{5}, we wait for the event empty from Tank-2 , and in states x_{3} and x_{4}, we wait for the event off from Heater. Consequently, we have already received empty if we are in x_{4} or x_{6}, and if we are in x_{5} or x_{6}, we have already received off. If the off event arrives, timer T_{1} is reset. After 4 time units, we make a transition from state x_{6} to x_{7} while sending the drain event to Tank-1 .

6.3 Verification

Verification means checking if a system fulfills some desired properties. The level of formalization in such checks has a wide range from “good faith” (no formal reasoning at all) to the use of formal proof systems like Hoare style assertions, automated proofs with systems like PVS [ORS92], or model checkers like KRONOS [OY93], UPPAAL [BLL^{+}96], or HyTech [HHWT95, HH95].

We take a look at some techniques suitable for our TCES model of the evaporator system. As said before, we are interested in verifying the following three properties:

1. If a cooling malfunction in the condenser occurs, the heater must be switched off fast enough such that the condenser does not explode.

2. If the heater is switched off, tank 1 is drained into tank 2 before the solution gets solid.

3. If valve 2 is opened to drain tank 1 into tank 2, tank 2 has to be empty.

From the definition of our modules it its clear that the “bad” things that should not happen only occur when control state x_{2} is reached in the TCES Pressure, x_{2} is reached in Tank-1 , or x_{3} is reached in Tank-2 . Furthermore, we know from the definition of the condition output functions that reaching one of these states is equivalent with sending the too-high symbol via component StatusPressure, solid via StatusTank-1, or overflow via StatusTank-2.

Thus, there are two possibilities to look for the unwanted things: We can either check the reachability of the control states mentioned above, or we can look for the occurrence of the three condition symbols too-high, solid, and overflow in the signals of the compound system.

6.3.1 Using Timing Diagrams

Our first attempt to verify the three properties makes use of timing diagrams, which show a graphical representation of the system’s signals. They are used to visualize the timing dependencies of different signals. If some signals are related, i.e., some symbol in a signal can only occur in a certain time range before or after some other symbol occurs in another signal, this relationship is shown in the diagram.

Figure 6.15 shows a timing diagram for the evaporator system. Vertically stacked we have all event components in our system; grouped from bottom to top are the output components names of D_{Condenser}, D_{Pressure}, D_{Tank-1} , D_{Tank-2} , D_{Controller}, and D_{Heater}. The right part of the diagram shows the occurrences of all proper events of the components’ alphabets. Time progress is drawn from left to right. Note that we have no linear scaling in the diagram.

The first proper event occurring in our system is Malfunction : mal^{1} from Condenser, denoting that the condenser starts malfunctioning. We denote this point in time with t_{0}. The event mal triggers two other events: In

1We use the same notation for events as in the graphical representation for TCESs.

[figure: t; t_{0}; t_{1}; t_{2}; t_{3}; t_{4}; Malfunction; Res_{T_{P}}; (1); 0 < Δt ≤ 8; Res_{T_{T 1}}; (2); 0 < Δt ≤ 4; Res_{T_{T 2}}; (3); Δt > 10; Empty; 0 < Δt ≤ 10; Res_{T_{1}}; Res_{T_{2}}; Δt > 2; Switch; 0 < Δt ≤ 3; Drain-1; Δt = 4; Drain-2; 0 < Δt ≤ 1; Res_{T_{H}}; Heat; Δt = 5]

Figure 6.15: A timing diagram for the evaporator system

Pressure, we change from state x_{0} to x_{1}, resetting timer T_{P}. After more than 8 time units the transition to state x_{2} may be taken, violating property 1 (the condenser should not explode). Thus, we must verify that the event Heat : off occurs within 8 time units. We denote this by (1) in the diagram.

The event mal also triggers in Controller the transition from state x_{0} to x_{1}, resetting timer T_{1}. Within 1 time unit, Controller takes the transition from x_{1} to x_{2} at time t_{1} ∈ (t_{0}, t_{0} + 1], sending the event Drain-2 : drain to Tank-2 and resetting timer T_{2}. Tank-2 also resets its timer T_{T_{2}}, and within 10 time units, the event Empty : empty will be sent. If the event Drain-1 : drain occurs within 10 time units after t_{1}, Tank-2 may change to state x_{3}, violating property 3 (tank 2 should not overflow). Therefore, we must ensure that the event Drain-1 : drain occurs more than 10 time units after t_{1}. We denote this by (3) in the diagram.

In Figure 6.15, we do not consider the case that in Controller the transition from state x_{2} to x_{4} is taken, which is possible if the draining of tank 2 takes 3 or less time units. A different timing diagram has to be drawn for this case.

Controller moves on from state x_{2} to x_{3}, generating the event Switch : off, if the value of timer T_{1} is at most 3 and T_{2} shows more than 2 time units.

Therefore, we have two edges ending at the Switch : off event at time t_{2} in our timing diagram. The timing is described by t_{2} ≤ 3 and t_{2} > t_{1} + 2. The off event triggers the transition from state x_{0} to x_{1} in Heater, which resets its timer T_{H}. After exactly 5 time units, Heater changes its state to x_{2}, sending the event Heat : off at time t_{3} = t_{2} + 5.

In the meantime, Controller uses its states x_{3}, x_{4}, x_{5} and x_{6} to wait for the events Heat : off and Empty : empty to occur. When the off event is occurs at time t_{3}, Controller resets its timer T_{1}, and Tank-1 resets its timer T_{T_{1}} while changing the state to x_{1}. After more than 4 time units, Tank-1 may go to state x_{2}, violating property 2 (the solution in tank 1 must not become solid). Thus, we must verify that the event Drain-1 : drain occurs within 4 time units. We denote this by (2) in the diagram.

Let us look at time t_{2} again. Controller is in state x_{3}. To get to state x_{7}, we must get to state x_{6} within 4 time units, since the event Ala_{T_{1}} : Ala_{3} occurs at time t_{4} = t_{3}+4, and if we are not at state x_{6} at time t_{4}, event Drain-1 : drain is not sent, eventually leading to a violation of property 2. Therefore, event Empty : empty must occur between t_{2} and t_{4}. Our diagram considers the case that empty occurs at a time t > t_{2}. We have to show t < t_{4}. From the timing in Tank-2 , we know that t − t_{1} ≤ 10, and we also know t_{4} = t_{3} + 4, t_{3} = t_{2} + 5, and t_{2} > t_{1} + 2. This yields t_{4} = t_{2} + 9 > t_{1} + 11 > t_{1} + 10 ≥ t.

Thus, Controller is at state x_{6} when the event Ala_{T_{1}} : Ala_{3} occurs at time t_{4} and go to state x_{7}, sending Drain-1 : drain.

It remains to check the requirements (1), (2), and (3) in the diagram. By 0 < t_{2} ≤ 3 and t_{3} = t_{2} + 5, we have 0 < t_{3} ≤ 8, showing (1). By t_{4} = t_{3} + 4, we have (2): 0 < t_{4} − t_{3} ≤ 4. And t_{2} > t_{1} + 2, t_{3} = t_{2} + 5, and t_{4} = t_{3} + 4 yields t_{4} − t_{1} > 11, which is sufficient for (3).

We have proven the three properties we expected from our system. We left out another timing diagram which is more simple, but has also to be checked. The advantages of this visual way of handling timing restrictions are not obvious if too many signals are involved, which leads to very large diagrams. Nevertheless, timing diagrams are widely used for various purposes like the verification of communication protocols, schedules for an automated production, or the design of railroad timetables.

6.3.2 Using Timed Automata

In [Huu98], an effective transformation from a TCES to an equivalent timed automaton is given (see also [HLU^{+}97a, HLU^{+}97b]). Equivalence in this case is expressed by means of a relation between timed languages of timed automata and sets of behaviors of TCESs. This transformation has been used in the KONDISK project to build six timed automata which are equivalent to the six TCES modules of the evaporator system [HLL^{+}98].

Since the product of these timed automata is equivalent to the discrete parallel interconnection of the TCESs, and since the state spaces are also comparable, the verification tool KRONOS [OY93] has been used as a model checker to verify that none of the three “bad” states is reachable. Another tool that was used successfully was HyTech [HHWT95, HH95].

6.3.3 Using the Parallel Interconnection Operator

Since we modeled our system as a set of interconnected TCESs, it is sensible to apply the parallel interconnection operator to obtain one TCES T having the semantics of the compound system.

When we have constructed such a TCES T , we can use both techniques mentioned above to verify the desired properties, or we can do the verification on the semantics of T . The semantic formalization of the three properties is simple, since we have introduced condition output signals which denote the control states of the modules. Thus, a signal-based version of the properties just says that the “bad” states are never reached:

1. ∀s ∈ S_{T} : ∀t ∈ ℝ_{≥0} : sȲ(t)(StatusPressure) ≠ too-high

2. ∀s ∈ S_{T} : ∀t ∈ ℝ_{≥0} : sȲ(t)(StatusTank-1) ≠ solid

3. ∀s ∈ S_{T} : ∀t ∈ ℝ_{≥0} : sȲ(t)(StatusTank-2) ≠ overflow

If we try to check the multiple solution property, the first part is trivial: Since the have no condition signals between the modules at all, the set of conditions names C^{io} (see Definition 4.12) is empty. Thus, the set of evaluations y of C^{io} we have to find in the multiple solution property is always Σ_{C^{io}} which contains just the evaluation y = ∅.

In the second part, we have to find solutions for the events between the modules. Since every event generated by a module in our system is received by one or more modules, we have E^{io} = {Malfunction, Drain-1, Drain-2, Empty, Switch, Heat}. Now we have to find for any combination of pre-states in the modules and any combination of post-states in the modules at least one z ∈ Σ_{E^{io}} which is a solution for the events between the modules.

This is the point where we face the state explosion problem. Each module has between 2 and 8 states, leading to a total of 2304 possible combinations of states. Since any combination of a pre- and a post-state has to be checked, we end up with over 5 million combinations. And for each of the combinations, the number of candidates for a solution is |Σ_{E^{io}}| = 64.

However, if we take a close look at the TCES definitions of our modules, we do not need to combine all six modules to verify the properties. Take property 3: It says that tank 2 has to be empty before tank 1 is drained. Looking at Figure 6.6, we see that tank 2 is empty (state x_{1}) if and only if Tank-2 has sent Empty : empty and Drain-1 : drain has not yet been received. On the other hand, Figure 6.14 shows that there is only one transition where Drain-1 : drain is sent; this is when changing from state x_{6} to x_{7}. Furthermore, state x_{6} can only be reached if Empty : empty was received earlier.

We conclude that for verifying property 3, it is sufficient to combine the TCESs Tank-2 and Controller by using the parallel interconnection operator. The resulting TCES can be checked against property 3. Analogously, the verification of property 1 only needs the TCESs Condenser, Pressure, Heater, and Controller, and for property 2, we need Heater, Tank-1 , Tank-2 , and Controller. This leads to a significant reduction of states and evaluations to be looked at.

Unfortunately, all three compositions above are quite large; therefore, we only show the discrete parallel interconnection of Pressure and Condenser to give an impression of how this works.

6.3.3.1 Composing Pressure and Condenser

Recall the definitions of the TCES Pressure and the DCES Condenser, especially their transition and output functions depicted in Figures 6.12 and 6.10. We apply the discrete parallel interconnection with unique solutions to Pressure and Condenser. Note that Condenser can be expressed as a TCES without clocks (see Lemma 5.7).

The validity of the unique solution property can be checked easily. Defining PressCond = Pressure∥Condenser, we get

PressCond = (\begin{matrix}∅, \{Heat\}, \{StatusPressure, StatusCondenser\}, \\ \{Malfunction\}, \{T_{P} \}, D_{PressCond}) \end{matrix}

with

D_{PressCond} = (\begin{matrix}\{Int_{T_{P}} \}, \{Heat, Ala_{T_{P}} \}, \\ \{(x_{0}, x_{0}), (x_{1}, x_{0}), (x_{2}, x_{0}), (x_{0}, x_{1}), (x_{1}, x_{1}), (x_{2}, x_{1})\}, \\ \{StatusPressure, StatusCondenser\}, \{Malfunction, Res_{T_{P}} \}, \\ f_{P C}, g_{P C}, h_{P C}, \{(x_{0}, x_{0})\}). \end{matrix}

Figure 6.16 shows the block diagram of the TCES PressCond.

The functions f_{P C}, g_{P C}, and h_{P C} are depicted in Figure 6.17. In the upper half of each circle, there is the first component of the state identifier and f_{P C} (from Pressure), and in the lower part, there are the second components

PressCond [figure: Heat; Malfunction; StatusPressure; StatusCondenser]

Figure 6.16: Block diagram of the TCES PressCond

(from Condenser). An interesting transition is the one from state (x_{0}, x_{0}) to (x_{0}, x_{1}). It shows that we are not in danger when mal and off occur at the same time. This transition from x_{0} to x_{0} does also exist in Pressure, but there is no explicit edge for it in Figure 6.12. Note that the self-loop edge at state (x_{0}, x_{0}) allows us to stay at this state if the Heat : off event occurs. Without this edge, we must take the transition to (x_{0}, x_{1}) while sending the Malfunction : mal event.

States (x_{1}, x_{0}) and (x_{2}, x_{0}) are not reachable, since Pressure cannot leave x_{0} without receiving the mal event. We simply can remove these states from PressCond, yielding the system in Figure 6.18 having the same semantics as PressCond. Removing states that cannot be reached is another way of keeping the state space small when using the parallel composition operator.

6.3. Verification 111

[figure: x_{0}; normal; x_{0}; normal]

[figure: Heat : off]

[figure: x_{1}; danger; x_{0}; normal]

[figure: x_{2}; too-high; x_{0}; normal]

Int_{T_{P}} : Int_{1} \overline{}

\overline{}Heat : off

Heat : off, /Malfunction : mal

/Malfunction : mal

/Malfunction : mal

[figure]

Heat : 0 /Res_{T_{P}} : Res, Malfunction : mal

[figure: x_{0}; normal; x_{1}; fail; x_{1}; danger; x_{1}; fail; x_{2}; too-high; x_{1}; fail; Int_{T_{P}} : Int_{1}; Heat : off]

Figure 6.17: Discrete part of the TCES PressCond

[figure: x_{0}; normal; x_{0}; normal]

[figure: Heat : off]

Heat : off, /Malfunction : mal

[figure]

Heat : 0 /Res_{T_{P}} : Res, Malfunction : mal

[figure: x_{0}; normal; x_{1}; fail; x_{1}; danger; x_{1}; fail; x_{2}; too-high; x_{1}; fail; Int_{T_{P}} : Int_{1}; Heat : off]

Figure 6.18: The reachable discrete part of the TCES PressCond 112

Conclusion

Formal verification is a necessity for the design of safety critical systems. The acceptance and success of formal methods in system design however depends on the choice of the modeling formalism, which must orient itself by the field of application in which systems are verified.

In chemical engineering, systems are often specified using block diagrams to represent modules. Information is exchanged between these modules using signal flows. The behavior of the modules is often described informally, which makes the verification of such systems almost impossible.

A suitable formal framework in this field are discrete condition/event systems (DCESs), which are representable as block diagrams and exchange signals generated by finite-state transition systems. Though DCESs are widely used for modeling systems, compositional theories for their verification can rarely be found in the literature. Moreover, there are no composition operators given for the important class of timed condition/event systems (TCESs).

Our aim is to create a formal framework for the modular verification of DCESs and TCESs. Examining the existing operators feedback and cascade used in, e.g., [SK91], we find that these are difficult to handle and that they are unable to model certain interconnections between DCESs. Therefore, we define the parallel interconnection operator, which is able to express almost any given interconnection structure between DCESs. The avoidance of algebraic loops in the systems is done in two different ways, using a unique solution property and a multiple solution property. Furthermore, the parallel interconnection is extended to TCESs. Summarizing, we define a new composition operator for DCESs and TCESs which is general, powerful, and easy to use.

The example in Chapter 6 shows that we do not need to compose all modules of a given system to verify certain properties. This is an important observation, since a reduction of the number of modules leads to a significantly smaller state space in the composed part. Thus, this is a promising technique to cope with the state explosion problem. Further work lies in the exploitation of such techniques, and in giving general rules how and when to apply which technique to a given system.

We also need to define a temporal logic for TCESs to be able to specify time dependent properties of TCESs in a formal verification framework.

Within the KONDISK project, we are currently working on further improvements of the automatic translation from TCES to timed automata [HLL^{+}98]. A goal is to build a tool containing a graphical frontend for defining TCESs using block diagrams and transition graphs, and to specify properties in a temporal logic. The TCESs are transformed into timed automata, and the temporal logic formula is converted into the verification language of a model checker for timed automata, e.g., KRONOS. Then this model checker is used to verify the properties, and the results, like certain states or transitions falsifying a property, are presented in the graphical frontend. Using various state space reduction techniques, the tool should be able to verify systems of reasonable size.

Bibliography

[AD94] R. Alur and D. Dill. A theory of timed automata. In Proceedings of the 17th ICALP: Automata Languages and Programming, volume 126, pages 183–235. Springer-Verlag, 1994.

[BG90] A. Benveniste and P. Le Guernic. Hybrid dynamical systems theory and the Signal language. IEEE Transactions on Automatic Control, 35(5):535–546, May 1990.

[BG92] G. Berry and G. Gonthier. The Esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming, 19(2):87–152, November 1992.

[BLL^{+}96] J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and W. Yi. UPPAAL—a tool suite for automatic verification of real-time systems. In Hybrid Systems III, LNCS 1066, pages 232–243. Springer-Verlag, 1996.

[CPHP87] P. Caspi, D. Pilaud, N. Halbwachs, and J. Plaice. Lustre: a declarative language for programming synchronous systems. In 14th ACM Symposium on Principles of Programming Languages, München, January 1987.

[GGB87] T. Gauthier, P. Le Guernic, and L. Besnard. Signal, a delarative language for synchronous programming of real-time systems. In Proc. 3rd Conf. on Functional Programming Languages and Computer Architectures, volume 274. Springer-Verlag, 1987.

[Hal93] Nicolas Halbwachs. Synchronous Programming of Reactive Systems. Kluwer Academic Publishers, 1993.

[HdR86] J. Hooman and W.-P. de Roever. The quest goes on: towards compositional proof systems for CSP. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Current Trends in Concurrency, volume 224 of LNCS, pages 343–395. Springer-Verlag, 1986.

[HdR90] J. Hooman and W.P. de Roever. Design and verification in realtime distributed computing: An introduction to compositional methods. In Protocol, Specification, Testing and Verification, IX, pages 37–56. North-Holland, 1990.

[HH95] T.A. Henzinger and P.-H. Ho. HyTech: The Cornell hybrid technology tool. In Hybrid Systems II, LNCS 999, pages 265–294. Springer-Verlag, 1995.

[HHWT95] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: The next generation. In RTSS’95, pages 56–65, 1995.

[HLL^{+}98] R. Huuck, Y. Lakhnech, B. Lukoschus, L. Urbina, S. Engell, S. Kowalewski, and J. Preußig. Integrating timed condition/event systems and timed automata for the verification of hybrid systems. Journal of Parallel and Distributed Computing Practices, 1998.

[HLU^{+}97a] R. Huuck, Y. Lakhnech, L. Urbina, S. Engell, S. Kowalewski, and J. Preußig. Combining a computer science and control theory approach to the verification of hybrid systems. In WPDRTS’97, Geneva, Switzerland, 1997.

[HLU^{+}97b] R. Huuck, Y. Lakhnech, L. Urbina, S. Engell, S. Kowalewski, and J. Preußig. Comparing timed condition/event systems and timed automata. In HART’97, volume 1201 of LNCS, pages 81–86. Springer-Verlag, 1997.

[HNSY94] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111(2):193–244, 1994.

[Hoa85] C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall International, 1985.

[Huu98] R. Huuck. Transformation von Echtzeit-Bedingungs-/Ereignis-systemen in Echtzeitautomaten: Ein Weg zur automatischen Verifikation. Diplomarbeit (Master’s thesis), Christian-Albrechts-Universität zu Kiel, 1998.

[Kow95] S. Kowalewski. Modulare diskrete Anlagenmodellierung zum systematischen Steuerungsentwurf. PhD thesis, Fachbereich Chemietechnik, Universität Dortmund, 1995.

[Lev95] N. G. Leveson. Safeware: System Safety and Computers. Addison-Wesley, 1995.

[Mil80] R. Milner. A calculus for communicating systems. volume 92 of LNCS. Springer-Verlag, 1980.

[Mil89] R. Milner. Communication and Concurrency. International Series in Computer Science. Prentice-Hall, 1989.

[ORS92] S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748– 752. Springer-Verlag, 1992.

[OY93] A. Olivero and S. Yovine. KRONOS: A Tool for Verifying Real-Time Systems. User’s Guide and Reference Manual. VERIMAG, Grenoble, France, 1993.

[SK91] R.S. Sreenivas and B.H. Krogh. On condition/event systems with discrete state realizations. In Discrete Event Dynamic Systems: Theory and Applications 1, pages 209–236. Kluwer Academic Publishers, Boston, USA, 1991.

Hiermit erkläre ich, daß ich die vorliegende Diplomarbeit selbständig verfaßt und keine anderen als die angegebenen Quellen und Hilfsmittel verwendet habe.

Kiel, August 1998