=Paper=
{{Paper
|id=None
|storemode=property
|title=An Abstract Block Formalism for Engineering Systems
|pdfUrl=https://ceur-ws.org/Vol-1000/ICTERI-2013-p-448-463-SMSV.pdf
|volume=Vol-1000
|dblpUrl=https://dblp.org/rec/conf/icteri/Ivanov13
}}
==An Abstract Block Formalism for Engineering Systems==
https://ceur-ws.org/Vol-1000/ICTERI-2013-p-448-463-SMSV.pdf
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)