An Abstract Block Formalism for Engineering Systems? Ievgen Ivanov1,2 1 Taras Shevchenko National University of Kyiv, Ukraine 2 Paul Sabatier University, Toulouse, France ivanov.eugen@gmail.com Abstract. We propose an abstract block diagram formalism based on the notions of a signal as a time-varying quantity, a block as a signal transformer, a connection between blocks as a signal equality constraint, and a block diagram as a collection of interconnected blocks. It does not enforce implementation details (like internal state-space) or particular kinds of dynamic behavior (like alternation of discrete steps and contin- uous evolutions) on blocks and can be considered as an abstraction of block diagram languages used by engineering system designers. We study its properties and give general conditions for well-definedness of the operation of a system specified by a block diagram for each admissible input signal(s). Keywords. block diagram, signal transformer, semantics, engineering system Key Terms. Mathematical Model, Specification Process, Verification Process 1 Introduction Many software tools for developing control, signal processing, and communica- tion systems are based on block diagram notations familiar to control engineers. Examples include system design software Simulink [1], Scicos [2], Dymola [3], SCADE [4], declarative synchronous languages [5], some embedded program- ming languages [6, 7]. In such notations, a diagram consists of blocks (components) connected by links. Typically, blocks have input and output ports, and (directed) links connect output ports of one block with input ports of the same or another block. A block is interpreted as an operation which transforms input signals (i.e. time-varying quantities) flowing though its input ports into output signals. ? Part of this research has been supported by the project Verisync (ANR-10-BLAN- 0310), France. An Abstract Block Formalism for Engineering Systems 449 Wide applicability of block diagram notations makes them an interesting object of study from a theoretical perspective. Classical control theory and signal processing already provide some degree of formal treatment of block diagrams [8, 9], but this is normally not sufficient to handle such aspects of modern system design languages as mixing of analog and discrete-time blocks, partially defined block operations, non-numeric data processing, etc. To take these issues into account, researches developed formal semantics for various block diagram languages [10–13]. Some effort has been made to unify approaches taken by different engineering system modeling and analysis tools and make them interoperable by the use of exchange languages with well-defined semantics [14, 15] such as Hybrid System Interchange Format (HSIF) which gives semantics of hybrids systems in terms of dynamic networks of hybrid automata [16, 17]. Although hybrid automata-based approaches like HSIF can be used to give semantics to block diagram languages [18] and have many advantages (e.g. avail- ability of verification theory for hybrid automata), we consider them not entirely satisfactory from a theoretical standpoint for the following reasons: – Semantics of a system component (block) is based on the notion of a dy- namical system with an internal state, and so the components with the same externally observable behavior can be semantically distinguishable. In our opinion, this is not needed for a high-level semantics which does not intend to describe details of the component’s physical/logical implementation. – Semantics of a system has a computational nature: it describes a sequence of discrete steps, where a step may involve function computations, solving initial-value problems for differential equations (continuous evolution), etc. It may be adequate for certain classes of discrete-continuous systems, but it does not always capture the behavior of a physical realization of a system (and thus may conflict which the view of a system designer). For example, a Zeno execution [17] of a hybrid automaton can be described as an infinite sequence of discrete steps which takes a bounded total time (but each step takes a non-zero time). This normally does not correspond to the behavior of a physical system described by the automaton. In many cases this is caused by system modeling simplifications. The conflict is usu- ally resolved by applying a certain method of continuation of an execution beyond Zeno time (regularization, Fillipov solution, etc.) [19]. But an ex- tended execution is not, in fact, a sequence of discrete steps, as it resumes after the accumulation point. In our opinion, in the general case, the dynamic behavior of a system should not be restricted to a particular scheme like a sequence of discrete steps and continuous evolutions. The goal of this paper is to introduce abstract formal models for blocks and block diagrams which overcomes limitations of the classical control/signal- theoretic approach to them and does not enforce implementation details (like internal state-space) or particular kinds of dynamic behavior (like alternation of discrete steps and continuous evolutions) on blocks. 450 Ie. Ivanov These models can be used to identify the most general properties of block diagram languages which are valid regardless of implementation details. In par- ticular, in the paper we will give a general formulation and conditions for well- definedness of the operation of a system specified by a block diagram for each admissible input signal(s). To achieve our goal, we will use a composition-nominative approach [20]. The main idea of this approach is that semantics of a system is constructed from semantics of components using special operations called compositions, and the syntactic representation of a system reflects this construction. The paper is organized in the following way: – In Section 2 we give definitions of the auxiliary notions which are used in the rest of the paper. – In Section 3 we introduce abstract notions of a block, a connection, a block diagram, and a block composition. We show how they fit into a system design process and give conditions of well-definedness of the operation of a system specified by a block diagram for each admissible input signal(s). 2 Preliminaries 2.1 Notation We will use the following notation: N = {1, 2, 3, ...}, N0 = N ∪ {0}, R+ is the set of nonnegative real numbers, f : A → B is a total function from A to B, ˜ is a partial function from A to B, 2A is the power set of a set A, f |X is f : A→B the restriction of a function f to a set X. If A, B are sets, then B A denotes the set of all total functions from A to B. For a function f : A→B˜ the symbol f (x) ↓ (f (x) ↑) means that f (x) is defined (respectively undefined) on the argument x. We denote the domain and range of a function as dom(f ) = {x | f (x) ↓} and range(f ) = {y | ∃x f (x) ↓ ∧ y = f (x)} respectively. We will use the the same notation for the domain and range of a binary relation: if R ⊆ A × B, then dom(R) = {x | ∃ y (x, y) ∈ R} and range(R) = {y | ∃ x (x, y) ∈ R}. We will use the notation f (x) ∼ = g(x) for the strong equality (where f and g are partial functions): f (x) ↓ iff g(x) ↓ and f (x) ↓ implies f (x) = g(x). The symbol ◦ denotes a functional composition: (f ◦ g)(x) ∼ = g(f (x)). By T we denote the (positive real) time scale [0, +∞). We assume that T is equipped with a topology induced by the standard topology on R. Additionally, we define the following class of sets: T0 = {∅, T } ∪ {[0, x) | x ∈ T \{0}} ∪ {[0, x] | x ∈ T } i.e. the set of (possibly empty, bounded or unbounded) intervals with left end 0. 2.2 Multi-valued functions A multi-valued function [20] assigns one or more resulting values to each argu- ment value. An application of a multi-valued function to an argument is inter- preted as a nondeterministic choice of a result. An Abstract Block Formalism for Engineering Systems 451 Definition 1 ([20]). A (total) multi-valued function from a set A to a set B tm (denoted as f : A−→ B) is a function f : A → 2B \{∅}. Thus the inclusion y ∈ f (x) means that y is a possible value of f on x. 2.3 Named sets We will use a simple notion of a named set to formalize an assignment of values to variable names in program and system semantics. Definition 2. ([20]) A named set is a partial function f : V →W ˜ from a non- empty set of names V to a set of values W . In this definition both names and values are unstructured. A named set can be considered as a partial (”flat”) case of a more general notion of nominative data [20] which reflects hierarchical data organizations and naming schemes. We will use a special notation for the set of named sets: V W denotes the set of all named sets f : V →W ˜ (this notation just emphasises that V is interpreted as a set of names). We consider named sets equal, if their graphs are equal. An expression of the form [n1 7→ a1 , n2 7→ a2 , ...] (where n1 , n2 , ... are distinct names) denotes a named set d such that the graph of d is {(n1 , a1 ), (n2 , a2 ), ...}. A nowhere-defined named set is called an empty named set and is denoted as []. For any named sets d1 , d2 we write d1 ⊆ d2 (named set inclusion), if the graph of a function d1 is a subset of the graph of d2 . We extend set-theoretical operations of union ∪, intersection ∩ and difference \ to the partial operations on named sets in the following way: the result of a union (intersection, difference) of named sets (operation’s arguments) is a named set d such that the graph of d is the union (intersection, difference) of graphs of the arguments (if such d exists). 3 An Abstract Block Formalism 3.1 Abstract block Let us introduce abstract notions of a signal as a time-varying quantity and a block as a signal transformer. We will use a real time scale for signals, but we will not require them to be continuous or real-valued. So the signals can be piecewise-constant as well and can be used to represent discrete evolutions. Informally, a block (see Fig. 1) is a device which receives input signals and produces output signals. We call a collection of input (output) signals an input (resp. output) signal bunch. At each time moment (the value of) a given signal may be present or absent. In the general case, the presence of an input signal at a given time does not imply the presence of an output signal at the same or any other time moment. A block can operate nondeterministically, i.e. for one input signal bunch it may choose an output signal bunch from a set of possible variants. However, for any input signal bunch there exists at least one corresponding output signal 452 Ie. Ivanov bunch (although the values of all signals in it may be absent at all times, which means that the block does not produce any output values). Normally, a block processes the whole input signal bunch, and does or does not produce output values. However, in certain cases a block may not process the whole input signal bunch and may terminate at some time moment before its end. This situation is interpreted as an abnormal termination of a block (e.g. caused by an invalid input). Fig. 1. An illustration of a block with input signals x1 , x2 and output signals y1 , y2 . The plot displays example evolutions of input and output signals. The input and output signals are lumped into an input and output signal bunch respectively. Solid curves represent (present) signal values. Dashed horizonal segments indicate absence of a signal value. Dashed vertical lines indicate the right boundaries of the domains of signal bunches. Let us give formal definitions. Let W be a (fixed) non-empty set of values. Definition 3. (1) A signal is a partial function from T to W (f : T →W ˜ ). ˜ V W such (2) A V -signal bunch (where V is a set of names) is a function s : T → that dom(s) ∈ T0 . The set of all V -signal bunches is denoted as Sb(V, W ). (3) A signal bunch is a V -signal bunch for some V . (4) A signal bunch s is trivial, if dom(s) = ∅ and is total, if dom(s) = T . A trivial signal bunch is denoted as ⊥. An Abstract Block Formalism for Engineering Systems 453 (5) For a given signal bunch s, a signal corresponding to a name x is a partial function t 7→ s(t)(x). This signal is denoted as s[x]. (6) A signal bunch s1 is a prefix of a signal bunch s2 (denoted as s1  s2 ), if s1 = s2 |A for some A ∈ T0 . Note that  on V -signal bunches is a partial order (for an arbitrary V ). Later we will need generalized versions of the prefix relation for pairs and indexed families of pairs of signal bunches. For any signal bunches s1 , s2 , s01 , s02 let us denote (s1 , s2 ) 2 (s01 , s02 ) iff there exists A ∈ T0 such that s1 = s01 |A and s2 = s02 |A . For any indexed families of pairs of signal bunches (sj , s0j )j∈J and (s00j , s000 j )j∈J 0 J,2 00 000 of signal bunches let us denote (sj , sj )j∈J  (sj , sj )j∈J iff there exists A ∈ T0 such that sj = s00j |A and s0j = s000 j |A for all j ∈ J. It is easy to check that 2 is a partial order on pairs of signal bunches and J,2 is a partial order on J-indexed families of pairs of signal bunches. A block has a syntactic aspect (e.g. a description in a specification language) and a semantic aspect – a partial multi-valued function on signal bunches. Definition 4. (1) A block is an object B (syntactic aspect) together with an as- sociated set of input names In(B), a set of output names Out(B), and a total tm multi-valued function Op(B) : Sb(In(B), W )−→ Sb(Out(B), W ) (operation, semantic aspect) such that o ∈ Op(B)(i) implies dom(o) ⊆ dom(i). (2) Two blocks B1 , B2 are semantically identical, if In(B1 ) = In(B2 ), Out(B1 ) = Out(B2 ), and Op(B1 ) = Op(B2 ). (3) An I/O pair of a block B is a pair of signal bunches (i, o) such that o ∈ Op(B)(i). The set of all I/O pairs of B is denoted as IO(B) and is called the input-output (I/O) relation of B. An inclusion o ∈ Op(B)(i) means that o is a possible output of a block B on the input i. For each input i there is some output o. The domain of o is a subset of the domain of i. If o becomes undefined at some time t, but i is still defined at t, we interpret this as an error during the operation of the block B (the block cannot resume its operation after t). Definition 5. A block B is deterministic, if Op(B)(i) is a singleton set for each In(B)-signal bunch i. We interpret the operation of a block as a (possibly nondeterministic) choice of an output signal bunch corresponding to a given input signal bunch. However, we would also like to describe this choice as dynamic, i.e. that a block chooses the output signal values at each time t, and in doing so it cannot rely on the future values of the input signals (i.e. values of the input signals at times t0 > t). If a block is deterministic, this requirement can be formalized in the same way as the notion of a causal (or nonanticipative) input-output system [26]. Definition 6. A deterministic block B is causal iff for all signal bunches i1 , i2 and A ∈ T0 , o1 ∈ Op(B)(i1 ), o2 ∈ Op(B)(i2 ), the equality i1 |A = i2 |A implies o1 | A = o 2 | A . 454 Ie. Ivanov This means that the value of the output signal bunch at time t can depend only on the values of the input signal at times ≤ t. Some works in the domain of systems theory extend the notion of a causal (deterministic) system to nondeterministic systems. However, there is no unified approach to an extension of this kind. For example, in the work [21], a system, considered as a binary relation on (total) signals S ⊆ AT × B T , where T is a time domain (Mesarovic time system, [22]) is “non-anticipatory”, if itSis a union of (graphs of) causal (non-anticipatory) selections from S, i.e, S = {f : dom(S) → range(S) | f ⊆ S, f is causal}. In the work [23] the authors define another notion of a “non-anticipatory” or “causal” system in nondeterministic case. In the theory developed in the work [24], the authors use a similar notion of a “precausal” system, which is also defined in [22], as a generalization of the notion of a causal system to the nondeterministic case. In this work, we generalize the notion of a non-anticipatory system in sense of [23] to blocks and call such blocks nonanticipative, and generalize the notion of a non-anticipatory system in sense of [21] to blocks, but call such blocks strongly nonanticipative. We will show that strongly nonanticipative block is nonanticipative. We will consider the words “causal” and “nonanticipative” as synonyms when they are used informally, but we will distinguish them in the context of formal definitions to avoid a conflict with Definition 6. Note, however, that the notion of a strongly nonanticipative block defined below is very different from the notion of a ”strictly causal“ system, defined in some works [25] as a system which uses only past (but not current or future) values of the input signal(s) to produce a current value of the output signal(s). Definition 7. A block B is nonanticipative, if for each A ∈ T0 and i1 , i2 ∈ Sb(In(B), W ), if i1 |A = i2 |A , then {o|A | o ∈ Op(B)(i1 )} = {o|A | o ∈ Op(B)(i2 )}. Definition 8. A block B is a sub-block of a block B 0 (denoted as B E B 0 ), if In(B) = In(B 0 ), Out(B) = Out(B 0 ), and IO(B) ⊆ IO(B 0 ). Informally, a sub-block narrows nondeterminism of a block. Definition 9. A block B is strongly nonanticipative, if for each (i, o) ∈ IO(B) there exists a deterministic causal sub-block B 0 E B such that (i, o) ∈ IO(B 0 ). Informally, the operation of a strongly nonanticipative block B can be inter- preted as a two-step process: 1. before receiving the input signals, the block B (nondeterministically) chooses a deterministic causal sub-block B 0 E B (response strategy); 2. the block B 0 receives input signals of B and produces the corresponding output signals (response) which become the output signals of B. Intuitively, it is clear that in this scheme at any time the block B does not need a knowledge of the future of its input signals in order produce the corresponding output signals. An Abstract Block Formalism for Engineering Systems 455 Lemma 1. If B is a deterministic block, then B is causal iff B is nonanticipa- tive. Proof. Follows immediately from Definition 6. The following theorem gives a characterization of a nonanticipative block which does not rely on comparison of sets of signal bunches. Theorem 1. A block B is nonanticipative iff the following holds: (1) if (i, o) ∈ IO(B) and (i0 , o0 ) 2 (i, o), then (i0 , o0 ) ∈ IO(B); (2) if o ∈ Op(B)(i) and i  i0 , then (i, o) 2 (i0 , o0 ) for some o0 ∈ Op(B)(i0 ). Proof. (1) Assume that (1) and (2) are satisfied. Assume that A ∈ T0 , i1 , i2 ∈ Sb(In(B), W ), and i1 |A = i2 |A . Let o ∈ Op(B)(i1 ). Then from assump- tion (1) we have o|A ∈ Op(B)(i1 |A ), because (i1 |A , o|A ) 2 (i1 , o). More- over, i1 |A  i2 , because i1 |A = i2 |A . Thus (i1 |A , o|A ) 2 (i2 , o0 ) for some o0 ∈ Op(B)(i2 ) by assumption (2). It is not difficult to check that o|A ∈ {o00 |A | o00 ∈ Op(B)(i2 )}. Because i1 , i2 , A are arbitrary, B is nonanticipative by Definition 7. (2) Assume that B is nonanticipative. Let us prove (1). Assume that (i, o) ∈ IO(B) and (i0 , o0 ) 2 (i, o). Then i0 = i|A and o0 = o|A for some A ∈ T0 . Then i0 |A = (i|A )|A = i|A , whence o0 = o|A ∈ {o00 |A | o00 ∈ Op(B)(i)} = {o00 |A | o00 ∈ Op(B)(i0 )} by Definition 7. Then o0 = o00 |A for some o00 ∈ Op(B)(i0 ). Moreover, dom(o00 ) ⊆ dom(i0 ) ⊆ A. Thus o0 = o00 and (i0 , o0 ) ∈ IO(B). Let us prove (2). Assume that o ∈ Op(B)(i) and i  i0 . Then i = i0 |A for some A ∈ T0 . Then i|A = (i0 |A )|A = i0 |A , whence o|A ∈ {o00 |A | o00 ∈ Op(B)(i)} = {o00 |A | o00 ∈ Op(B)(i0 )} by Definition 7. Then o|A = o0 |A for some o0 ∈ Op(B)(i0 ). Moveover, dom(o) ⊆ dom(i) ⊆ A, whence o = o|A = o0 |A . Thus (i, o) 2 (i0 , o0 ). Theorem 2. (About strongly nonanticipative block) (1) If a block B is strongly nonanticipative, then it is nonanticipative. (2) There exists a nonanticipative block which is not strongly nonanticipative. Proof (Sketch). (1) Assume that B is strongly nonanticipative. Let R be the set of all re- lations R ⊆ IO(B) such that R is an I/O relation of a nonanticipative block. For each R ∈ IO let us define a block BR such that IO(BR ) = R, In(BR ) = In(B), Out(BR ) = Out(B). Let B = {BR | R ∈ R}. Then each element ofSB is nonanticipative. S From Definition 9 and Lemma 1 we have 0 IO(B) ⊆ R = B 0 ∈B IO(B S ). On the other hand, IO(B 0 ) ⊆ IO(B) for any B ∈ R, so IO(B) = B 0 ∈B IO(B 0 ). It is easy to see from Theorem 1 0 that (nonempty) union of I/O relations of nonanticipative block is an I/O relation of a nonanticipative block. Thus B is nonanticipative. 456 Ie. Ivanov (2) Assume that W = R. Let f : R → R be a function that is discontinuous at some point (e.g. a signum function). Let use define a block B such that In(B) = {x} and Out(B) = {y} for some names x, y, and for each i ∈ Sb(In(B), R), Op(B)(i) is defined as follows: • if dom(i[x]) = T and limt→+∞ i[x](t) exists and finite, then Op(B)(i) is the set of all {y}-signal bunches o such that dom(o) = dom(o[y]) = T and   lim o[y](t) = f lim i[x](t) ; t→+∞ t→+∞ • otherwise, Op(B)(i) is S the set of all {y}-signal bunches o such that dom(o) = dom(o[y]) = {A ∈ T0 | A ⊆ dom(i[x])}. Obviously, in this definition Op(B)(i) 6= ∅ (because T0 is closed under unions) and dom(o) ⊆ dom(i) for each o ∈ Op(B)(i). So B is indeed a block. Using Theorem 1 it is not difficult to show that B is nonanticipa- tive. Suppose that B has a a deterministic causal sub-block B 0 . Let a ∈ R and ak ∈ R, k = 1, 2, ... be a sequence such that limk→∞ ak = a. Let us show that limk→∞ f (ak ) = f (a). Let us define sequences ik ∈ Sb({y}, R), ok ∈ Sb({y}, R), and tk ∈ T , k = 1, 2, ... by induction as follows. Let i1 (t) = [x 7→ a1 ] for all t ∈ T , o1 be a unique member of Op(B 0 )(i1 ), and t1 = 0. If i1 , i2 , ..., ik are already defined, let ik+1 (t) = ik (t), if t ∈ [0, tk ] and ik+1 (t) = [x 7→ ak+1 ], if t ∈ T \[0, tk ]. Let ok+1 be a unique member of Op(B 0 )(ik+1 ). Because B 0 E B, dom(ok+1 ) = dom(ok+1 [y]) = T and limt→+∞ ok+1 [y](t) = f (limt→+∞ ik+1 [x](t)) = f (ak+1 ). Then let tk+1 = 1 + max{tk , inf{τ ∈ T | 1 sup{|ok+1 [y](t) − f (ak+1 )| | t ≥ τ } ≤ }} k+1 We have defined sequences ik , ok , tk . The sequence tk , k = 1, 2, ... is a strictly increasing and unbounded from above and t1 = 0. Let i be a {x}-signal bunch such that dom(i) = T , i(t1 ) = i1 (t1 ), and i(t) = ik+1 (t), if t ∈ (tk , tk+1 ], k ∈ N, and o be a (unique) member of Op(B 0 )(i). We have ik+1 [x](t) = ak+1 for all k = 1, 2, ... and t > tk . Then i[x](t) ∈ {ak+1 , ak+2 , ...} for all k ∈ N and t > tk . For each  > 0 there exists k ∈ N such that |ak0 − a| <  for all k 0 ≥ k, whence |i[x](t) − a| <  for all t > tk . Thus limt→+∞ i[x](t) = a. Then dom(o) = dom(o[y]) = T and limt→+∞ o[y](t) = f (a), because B 0 E B. On the other hand, ik+1 |[0,tk ] = ik |[0,tk ] for all k ∈ N. Because tk is an increasing sequence, we have ik0 |[0,tk ] = ik |[0,tk ] for all k and k 0 ≥ k. Be- sides, i|(tk ,tk+1 ] = ik+1 |(tk ,tk+1 ] for all k ∈ N, whence i|(tk ,tk+1 ] = ik0 |(tk ,tk+1 ] for all k 0 ≥ k + 1. Also, ik (t1 ) = i1 (t1 ) for all k ∈ N. Then i|[0,tk ] = i|{t1 }∪(t1 ,t2 ]∪...∪(tk−1 ,tk ] = ik |[0,tk ] for all k = 2, 3, ..., whence o|[0,tk ] = ok |[0,tk ] , because B 0 is causal. Then o(tk ) = ok (tk ) for all k = 2, 3, ..., and from the definition of tk we have |o[y](tk ) − f (ak )| = |ok [y](tk ) − f (ak )| ≤ k1 for all k = 2, 3, .... This implies that limk→∞ f (ak ) = f (a), because limt→+∞ o[y](t) = f (a). We conclude that f is sequentially continuous and thus is continuous. An Abstract Block Formalism for Engineering Systems 457 This contradicts our choice of f as a discontinuous function. Thus B has not deterministic causal sub-blocks. Consequently, B is not strongly nonantici- pative, though it is nonanticipative. The proof of this theorem gives a reason of why Definition 9 better captures a intuitive idea of causality than Definition 7. Consider, for example, the block B constructed in the proof of the item (2) of Theorem 2, when f is the signum function (i.e., f (0) = 0, f (x) = 1, if x > 0, and f (x) < 0, if x < 0). Then B outputs a signal which converges to 1 (as t → +∞) whenever the input signal converges to a positive number (as t → +∞). Moreover, it outputs a signal which converges to 0 whenever the input signal converges to 0. This implies that when the block receives a decreasing positive input signal which tends to 0, it decides to output values which are close to 0 starting from some time t. Intuitively, after reading the input signal until time t, the block decides that 0 is a more likely limit of the input signal than a positive value, but such a decision cannot be based on the past values of the input signal, so it requires some knowledge of the future of the input signal. These informal observations are captured by the fact that B has no deterministic causal sub-blocks. In the rest of the paper we will focus on strongly nonanticipative blocks, as more adequate models of (real-time) information processing systems. Consider an example of a strongly nonanticipative block. Let u, y be names. Assume that W = R. Example 1. Let B be a block such that In(B) = {u}, Out(B) = {y}, and for each i, Op(B)(i) = {o1 (i), o2 (i)}, where o1 (i), o2 (i) ∈ Sb(Out(B), W ) are signal bunches such that – dom(o1 (i)) = dom(o2 (i)) = dom(i); – o1 (i)(t) = [y 7→ i[u](t)] for all t ∈ dom(i); – o2 (i)(t) = [y 7→ 2i[u](t)] for all t ∈ dom(i). Informally, this means that B is a gain block with a slope which is either 1 or 2 during the whole duration of the block’s operation. Obviously, B satisfies Definition 4(1). Let us check that it is strongly nonan- ticipative. For j = 1, 2 let Bj Θ B be a sub-block such that Op(Bj )(i) = {oj (i)} for all i ∈ Sb(In(B), W ) (i.e. B1 always selects o1 (i) from Op(B)(i) and B2 always selects o2 (i)). The blocks B1 , B2 are deterministic and it is easy to see that they are causal. Obviously, each I/O pair (i, o) ∈ IO(B) belongs either to IO(B1 ), or to IO(B2 ), so B is strongly nonanticipative. Now let us consider an example of a block which is not nonanticipative. Example 2. Let B 0 be a block such that In(B 0 ) = {u}, Out(B 0 ) = {y}, and – Op(B 0 )(i) = {o1 }, where dom(o1 ) = dom(i) and o1 (t) = [y 7→ 1] for all t ∈ dom(i), if dom(i[u]) = T ; 458 Ie. Ivanov – Op(B 0 )(i) = {o2 }, where dom(o2 ) = dom(i) and o2 (t) = [y 7→ 0] for all t ∈ dom(i), otherwise. Informally, the block B 0 decides whether its input signal u is total. It is easy to see that B 0 indeed satisfies Definition 4(1), but the condition (1) of Theorem 1 is not satisfied, because (i, o) ∈ IO(B 0 ), where i(t) = [u 7→ 0] for all t ∈ T , o(t) = / IO(B 0 ). [y 7→ 1] for all t ∈ T , and (i|[0,1] , o|[0,1] ) 2 (i, o), but (i|[0,1] , o|[0,1] ) ∈ 0 So B is not nonanticipative. Informally, the reason is that at each time t the current value of y depends on the entire input signal. 3.2 Composition of blocks By connecting inputs and outputs of several (strongly nonanticipative) blocks one can form a larger block – a composition of blocks (see Fig. 2). We assume that an output can be connected to several inputs, but each input can be connected to no more than one output. Unconnected inputs and outputs of constituent blocks become inputs and output of the composition. Connections are interpreted as signal equality constraints and they always relate an output of some block (”source”) with an input of the same or another block (”target”). We represent connections in the graphical form (like in Fig. 2) as arrows connecting blocks. Fig. 2. An informal illustration of a block composition. Three blocks are composed to form a larger block (a dashed rectangle). Solid arrows denote connections between blocks. Dashed arrows denote unconnected inputs/outputs of the blocks 1, 2, 3 (which become the input/outputs of the dashed block). Definition 10. (1) A block diagram is a pair ((Bj )j∈J , ) of an indexed family of blocks (Bj )j∈J and an injective binary relation  ⊆ Vout × Vin , which is called an interconnection relation, where [ [ Vin = {j} × In(Bj ), Vout = {j} × Out(Bj ). j∈J j∈J An Abstract Block Formalism for Engineering Systems 459 Fig. 3. A strongly nonanticipative block B is composed to obtain a block B 0 (a dashed rectangle). A solid loop arrow denotes a connection between an output and an input of B. Dashed arrows denote unconnected inputs and outputs of B which become the inputs and outputs of B 0 . (2) A block diagram ((Bj )j∈J , ) is called regular, if each Bj , j ∈ J is strongly nonanticipative. Note that a diagram may consist of an infinite set of blocks. A relation (j, x)  (j 0 , x0 ) means that the output x of the j-th block is connected to the input x0 of the j 0 -th block. A block diagram is only a syntactic aspect of a block composition. We define semantics of a block composition only for strongly nonanticipative blocks. To describe it informally consider Fig. 3. The connection between y2 and x2 means a signal equality constraint. The block B chooses (nondeterministically) some deterministic sub-block B0 E B. When a signal starts flowing into the input x1, the block B 0 tries to choose the initial values for the signals of y1, y2, x2 so that they satisfy the operation of the block B0 (Op(B0 )) and the signals of x2 and y2 have the same values. If such initial values do not exist, the block B 0 terminates (the output signal bunch is nowhere defined). Otherwise, B 0 continues to operate in the similar way until either the signals of y1, y2, x2 cannot be continued, or the input signal (x1) ends. Definition 11. Let ((Bj )j∈J , ) be a regular block diagram. A block B is a composition of (Bj )j∈J under the interconnection relation , if S – In(B) = ( S j∈J {j} × In(Bj ))\range(), – Out(B) = ( j∈J {j} × Out(Bj ))\dom(), – Op(B)(i) is the set of all Out(B)-signal bunches o such that there exist deterministic causal sub-blocks Bj0 E Bj , j ∈ J and an indexed family (ij , oj )j∈J ∈ Xm (i) such that (1) dom(o) = dom(oj ) for all j ∈ J, (2) o[(j, x)] = oj [x] for all (j, x) ∈ Out(B), where Xm (i) is the set of J,2 -maximal elements of X(i), and X(i) is the set of all indexed families of pairs of signal bunches u = (ij , oj )j∈J such that (3) dom(ij ) = dom(oj ) = dom(ij 0 ) = dom(oj 0 ) ⊆ dom(i) for all j, j 0 ∈ J, (4) ij [x] = i|dom(ij ) [(j, x)] for each (j, x) ∈ In(B), (5) (ij , oj ) ∈ IO(Bj0 ) for each j ∈ J, 460 Ie. Ivanov (6) (j, x)  (j 0 , x0 ) implies oj [x] = ij 0 [x0 ]. In this definition, ij and oj denote the input and output signal bunches of the j-th block. The set Xm (i) contains maximally extended (in sense of the relation J,2 ) indexed families of signal bunches defined on a subset of the domain of i (the input signal bunch of B) which satisfy constraints imposed by the intercon- nection relation. Any such family gives a possible output of B for the given i by the condition (2), i.e. output signals of B are obtained from the output signals of the sub-blocks Bj0 . It is clear that any two compositions of (Bj )j∈J under  are semantically identical. Lemma 2. (Continuity of the operation of a causal deterministic causal block). Let B be a deterministic causal block. Let c ⊆ Sb(In(B), W ) be a non-empty -chain, i∗ beSits supremum (in sense of ), and o∗ ∈ Op(B)(i∗ ). Then o∗ is a supremum of i∈c Op(B)(i) (in sense of ). Proof. Follows from Definition 6. Theorem 3. Let ((Bj )j∈J , ) be a regular block diagram. Then (1) A composition of (Bj )j∈J under  exists. (2) If B is a composition of (Bj )j∈J under , then B is strongly nonanticipa- tive. The proof follows from Lemma 2 and Definition 11. 3.3 Specification and implementation Above we have considered a block as an abstract model of a real component. However, it can also be considered as a specification of requirements for a compo- nent. Let B spec , B impl be two strongly nonanticipative blocks. Let us call them a specification block and implementation block respectively. Definition 12. B impl is a refinement of B spec , if B impl is a sub-block of B spec . I.e. an implementation should have the the same input and output names as a specification, and for each input, an output of an implementation should be one of the possible outputs of a specification. We generalize this to diagrams. Let D = ((Bj )j∈J , ) and D0 = ((Bj0 )j∈J 0 , 0 ) be regular block diagrams. Definition 13. D is a refinement of D0 , if J = J 0 , Bj is a refinement of Bj0 for each j ∈ J, and the relations  and 0 coincide. Theorem 4. (Compositional refinement) Let B be a composition of (Bj )j∈J under  and B 0 be a composition of (Bj0 )j∈J 0 under 0 . If D is a refinement of D0 , then B is a refinement of B 0 . The proof follows from Definition 9, 11, and transitivity of the sub-block relation. This theorem can be considered as a foundation of a modular approach [29, 30] to system design: An Abstract Block Formalism for Engineering Systems 461 1. Create specifications of the system components (Bj0 , j ∈ J 0 ) and connect them (0 ), as if they were real components. 2. Analyze a composition of specifications (B 0 ) to ensure that any of its imple- mentations (B 00 E B 0 ) satisfies requirements to the final system. 3. Create an implementation (Bj ) for each specification (Bj0 ). 4. Connect implementations (according to 0 ). Then the composition of im- plementations (B) is a final system which satisfies design requirements. We consider the steps 1 and 3 domain- and application-specific. The conclusion of the step 4 is addressed in Theorem 4. Step 2 requires some verification method which depends on the nature of requirements. One of the most basic and common requirements is that the operation of B 0 is defined on all input signal bunches which are possible in the context of a specific application of this composition. This trivially holds because of Theorem 3 and our definition of a block. However, B 0 may terminate abnormally on some or all input signal bunches of interest (as we have noted, we interpret the situ- ation when o ∈ Op(B̃)(i) and dom(o) ⊂ dom(i) for some block B̃ as abnormal termination of B̃ on i). So the requirement can be reformulated as follows: B 0 never terminates abnormally on any input signal bunch from a given set IN (this implies that the same property holds for B). We will call this property as well-definedness of the operation of B 0 on IN and study it in the next subsection. 3.4 Well-definedness of the operation of a composition of blocks Let B be a block and IN be some set of In(B)-signal bunches. Definition 14. The operation of B is well-defined on IN , if dom(i) = dom(o) for each i ∈ IN and o ∈ Op(B)(i). Let D = ((Bj )j∈J , ) be a regular block diagram and B be a composition of (Bj )j∈J under . Let F be the set of all families of blocks of the form (Bj0 )j∈J , where for each j ∈ J, Bj0 is a deterministic causal sub-block of Bj . For each In(B)-signal bunch i and a family of blocks F = (Bj0 )j∈J let X F (i) be the set of all indexed families of pairs of signal bunches u = (ij , oj )j∈J which satisfy conditions (3)-(6) of Definition 11 (for B and (Bj0 )j∈J ). F Let Xm (i) denote the set of all J,2 -maximal elements of X F (i). For any indexed family of signal bunches u = (ij , oj )j∈J let O(u) denote the set of all Out(B)-signal bunches o which satisfy conditions (1)-(2) of Definition 11. For any u = (ij , oj )j∈J ∈ X F (i), the domains of ij , oj for all j ∈ J coincide. Denote by cdom(u) this common domain (we assume cdom(u) = T , if J = ∅). S S From Definition 11 we have Op(B)(i) = F ∈F u∈X F (i) O(u) for each i. m Then from Definition 14 we get the following simple criterion: Theorem 5. The operation of B is well-defined on IN iff for each i ∈ IN , F ∈ F , and u ∈ X F (i), if cdom(u) ⊂ dom(i), then u ∈ F / Xm (i). 462 Ie. Ivanov This criterion means that B is well-defined, if each u ∈ X F (i), the common domain of which does not cover dom(i), is extendable to a larger u0 ∈ X F (i) (in sense of J,2 ). We will call it a local extensibility criterion, because, basically, to prove well-definedness, we only need to show that the members of the family u can be continued onto a time segment [0, sup cdom(u) + ] for some small  > 0 (under constraints imposed by the interconnection relation ). Locality is especially useful when a block diagram contains ”delay” blocks (possibly working as variable delays), because constraints imposed by connections between blocks reduce over small time intervals. A drawback of this criterion is that it requires checking local extensibility of signal bunches satisfying the I/O relations (IO(Bj0 )) of arbitrarily chosen deterministic causal sub-blocks Bj0 E Bj (condition (5) of Definition 11), which are not explicitly expressed in terms of I/O relations of Bj , j ∈ J. For this reason, we seek for a condition of well-definedness in terms of I/O relations of the constituents of the composition (IO(Bj ), j ∈ J). Let X(i) denote the set X F (i), where F = (Bj )j∈J . Note that F may not be a member of F . Theorem 6. The operation of B is well-defined on IN iff for each i ∈ IN and u ∈ X(i) there exists u0 ∈ X(i) such that u J,2 u0 and cdom(u0 ) = dom(i). The proof follows from Theorem 5 and Definition 9. References 1. Simulink - Simulation and Model-Based Design, http://www.mathworks.com/ products/simulink 2. Campbell, S.L., Chancelier, J.-P., Nikoukhah, R.: Modeling and Simulation in Scilab/Scicos with ScicosLab 4.4. Springer (2010) 3. Multi-Engineering Modeling and Simulation – Dymola, http://www.3ds.com/ products/catia/portfolio/dymola 4. SCADE Suite, http://www.esterel-technologies.com/products/scade-suite 5. Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: LUSTRE: A declarative language for programming synchronous systems. In: 14th Annual ACM Symp. on Principles of Programming Languages, Munich, Germany, pp. 178-188 (1987) 6. Henzinger, T., Horowitz, B., Kirsch, C.: Giotto: A Time-Triggered Language for Embedded Programming. First International Workshop on Embedded Software, EMSOFT’01, pp. 166-184 (2001) 7. Lublinerman, R., Tripakis, S.: Modular Code Generation from Triggered and Timed Block Diagrams. In: IEEE Real-Time and Embedded Technology and Ap- plications Symposium, pp. 147-158 (2008) 8. Sontag, E.D.: Mathematical Control Theory: Deterministic Finite Dimensional Systems. Second Edition, Springer, New York (1998) 9. Proakis, J., Manolakis, D.: Digital Signal Processing: Principles, Algorithms and Applications, 4th ed. Pearson (2006) 10. Tiwari, A.: Formal semantics and analysis methods for Simulink Stateflow models. Unpublished report, SRI International (2002) An Abstract Block Formalism for Engineering Systems 463 11. Bouissou, O., Chapoutot, A.: An operational semantics for Simulink’s simulation engine. LCTES 2012, pp. 129-138. (2012) 12. Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. Electronic Notes in The- oretical Computer Science 109, 43-56 (2004) 13. Marian, N., Ma, Y.: Translation of Simulink Models to Component-based Software Models. In: 8-th Int. Workshop on Research and Education in Mechatronics, 14-15 June 2007, Talin University of Technology, Estonia (2007) 14. Pinto, R., Sangiovanni-Vincentelli, A., Carloni L.P., Passerone, R.: Interchange formats for hybrid systems: Review and proposal. In: HSCC 05: Hybrid Systems Computation and Control. Springer-Verlag, pp. 526–541 (2005) 15. Beek, D.A., Reniers, M.A., Schiffelers, R.R., Rooda, J. E.: Foundations of a Com- positional Interchange Format for Hybrid Systems. In: HSCC’07, pp. 587-600 (2007) 16. Henzinger, T.: The theory of hybrid automata. In: IEEE Symposium on Logic in Computer Science, pp. 278–292 (1996) 17. Goebel, R., Sanfelice, R., Teel, R.: Hybrid dynamical systems. In: IEEE Control Systems Magazine 29, 29–93 (2009) 18. Schrammel, P., Jeannet, B.: From hybrid data-flow languages to hybrid automata: a complete translation. In: HSCC 2012: pp. 167–176 (2012) 19. Camhbel, M.,K., Heemels, A.J., van der Schaft, A.J., Schumacher, J.M.: Solution concepts for hybrid dynamical systems. In: Proc. IFAC 15th Triennial World Congress, Barcelona, Spain (2002) 20. Nikitchenko, N.S.: A composition nominative approach to program semantics. Technical report IT-TR 1998-020, Technical University of Denmark, 103 p. (1998) 21. Windeknecht, T.G.: Mathematical systems theory: Causality. Mathematical sys- tems theory 1, pp. 279-288 (1967) 22. Mesarovic, M.,D., Takahara, Y.: Abstract systems theory. Springer, Berlin Hei- delberg New York, 439 p. (1989) 23. Foo, N., Peppas, P.: Realization for Causal Nondeterministic Input-Output Sys- tems. Studia Logica 67, pp. 419-437 (2001) 24. Lin, Y.: General systems theory: A mathematical approach. Springer, 382 p. (1999) 25. Matsikoudis, E., Lee, E.: On Fixed Points of Strictly Causal Functions. Tech- nical report UCB/EECS-2013-27, EECS Department, University of California, Berkeley (2013). 26. Williems, J.: Paradigms and puzzles in the theory of dynamical systems. In: IEEE Transactions on Automatic Control 36, pp. 259-294 (1991) 27. Williems, J.: On Interconnections, Control, and Feedback. In: IEEE Transactions on Automatic Control 42, pp. 326-339 (1997) 28. Williems, J.: The behavioral approach to open and interconnected systems. In: IEEE Control Systems Magazine, pp. 46-99 (2007) 29. Baldwin, C.Y., Clark, K.B.: Design Rules, Volume 1: The Power of Modularity. MIT Press (2000) 30. Tripakis, S., Lickly, B., Henzinger, T., Lee, E.: On relational interfaces. Proceed- ings of EMSOFT’2009, pp. 67-76 (2009) 31. Ivanov, Ie.: A criterion for global-in-time existence of trajectories of non- deterministic Markovian systems. Communications in Computer and Information Science 347, pp. 111-130, Springer (2012) 32. Carloni, L.P., Passerone, R., Pinto A.: Languages and Tools for Hybrid Systems Design. Foundations and Trends in Design Automation 1, 1-204 (2006)