The Refinement Calculus of Reactive Systems∗
Viorel Preoteasa

Iulia Dragomir

Stavros Tripakis

arXiv:1710.03979v2 [cs.LO] 8 Feb 2018

February 9, 2018

Abstract
The Refinement Calculus of Reactive Systems (RCRS) is a compositional formal framework for modeling and reasoning about reactive systems. RCRS provides a language which allows to describe atomic
components as symbolic transition systems or QLTL formulas, and composite components formed using
three primitive composition operators: serial, parallel, and feedback. The semantics of the language
is given in terms of monotonic property transformers, an extension to reactive systems of monotonic
predicate transformers, which have been used to give compositional semantics to sequential programs.
RCRS allows to specify both safety and liveness properties. It also allows to model input-output systems
which are both non-deterministic and non-input-receptive (i.e., which may reject some inputs at some
points in time), and can thus be seen as a behavioral type system. RCRS provides a set of techniques
for symbolic computer-aided reasoning, including compositional static analysis and verification. RCRS
comes with a publicly available implementation which includes a complete formalization of the RCRS
theory in the Isabelle proof assistant.

Contents
1 Introduction
1.1 Novel contributions of this paper and relation to our prior work . . . . . . . . . . . . . . . . .

3
4

2 Preliminaries

5

3 Language
3.1 An Algebra of Components . . . . . . . . . . . .
3.2 Symbolic Transition System Components . . . .
3.2.1 General STS Components . . . . . . . . .
3.2.2 Variable Name Scope . . . . . . . . . . .
3.2.3 Stateless STS Components . . . . . . . .
3.2.4 Deterministic STS Components . . . . . .
3.2.5 Stateless Deterministic STS Components
3.3 Quantified Linear Temporal Logic Components .
3.3.1 QLTL . . . . . . . . . . . . . . . . . . . .
3.3.2 QLTL Components . . . . . . . . . . . . .
3.4 Well Formed Composite Components . . . . . . .

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.

6
6
7
7
9
10
10
11
11
12
13
14

∗ The bulk of this work was done while Preoteasa and Dragomir were at Aalto University. Preoteasa is currently at Space
Systems Finland. Dragomir is currently at Verimag. Tripakis is affiliated with Aalto University and the University of California
at Berkeley. This work was partially supported by the Academy of Finland and the U.S. National Science Foundation (awards
#1329759 and #1139138). Dragomir was supported during the writing of this paper by the Horizon 2020 Programme Strategic
Research Cluster (grant agreement #730080 and #730086).

1

4 Semantics
4.1 Monotonic Property Transformers . . . . . . . . . . . . . . . . . . . . . . . . .
4.1.1 Some Commonly Used MPTs . . . . . . . . . . . . . . . . . . . . . . . .
4.1.2 Operators on MPTs: Function Composition, Product, and Fusion . . .
4.1.3 Novel Operators Used in Semantical Definition of Feedback . . . . . . .
4.1.4 Refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2 Subclasses of MPTs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.1 Relational MPTs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.2 Guarded MPTs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2.3 Other subclasses and overview . . . . . . . . . . . . . . . . . . . . . . .
4.3 Semantics of Components as MPTs . . . . . . . . . . . . . . . . . . . . . . . . .
4.3.1 Example: Two Alternative Derivations of the Semantics of Diagram Sum
4.3.2 Characterization of Legal Input Traces . . . . . . . . . . . . . . . . . . .
4.3.3 Semantic Equivalence and Refinement for Components . . . . . . . . . .
4.3.4 Compositionality Properties . . . . . . . . . . . . . . . . . . . . . . . . .

. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
. . . .
of Fig.
. . . .
. . . .
. . . .

. .
. .
. .
. .
. .
. .
. .
. .
. .
. .
2.
. .
. .
. .

.
.
.
.
.
.
.
.
.
.
.
.
.
.

.
.
.
.
.
.
.
.
.
.
.
.
.
.

15
15
15
17
17
18
19
19
20
20
21
22
23
24
24

5 Symbolic Reasoning
5.1 Symbolic Transformation of STS Components to QLTL Components . . . . . . . . . . . . . .
5.2 Symbolic Transformations of Special Atomic Components to More General Atomic Components
5.3 Symbolic Computation of Serial Composition . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.3.1 Symbolic Serial Composition of Two QLTL Components . . . . . . . . . . . . . . . . .
5.3.2 Symbolic Serial Composition of Two General STS Components . . . . . . . . . . . . .
5.3.3 Symbolic Serial Composition of Two Stateless STS Components . . . . . . . . . . . .
5.3.4 Symbolic Serial Composition of Two Deterministic STS Components . . . . . . . . . .
5.3.5 Symbolic Serial Composition of Two Stateless Deterministic STS Components . . . .
5.3.6 Symbolic Serial Composition of Two Arbitrary Atomic Components . . . . . . . . . .
5.3.7 Correctness of Symbolic Serial Composition . . . . . . . . . . . . . . . . . . . . . . . .
5.4 Symbolic Computation of Parallel Composition . . . . . . . . . . . . . . . . . . . . . . . . . .
5.4.1 Symbolic Parallel Composition of Two QLTL Components . . . . . . . . . . . . . . .
5.4.2 Symbolic Parallel Composition of Two General STS Components . . . . . . . . . . . .
5.4.3 Symbolic Parallel Composition of Two Stateless STS Components . . . . . . . . . . .
5.4.4 Symbolic Parallel Composition of Two Deterministic STS Components . . . . . . . . .
5.4.5 Symbolic Parallel Composition of Two Stateless Deterministic STS Components . . .
5.4.6 Symbolic Parallel Composition of Two Arbitrary Atomic Components . . . . . . . . .
5.4.7 Correctness of Symbolic Parallel Composition . . . . . . . . . . . . . . . . . . . . . . .
5.5 Symbolic Computation of Feedback Composition for Decomposable Deterministic STS Components . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.5.1 Decomposable Components . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.5.2 Symbolic Feedback of a Decomposable Deterministic STS Component . . . . . . . . .
5.5.3 Symbolic Feedback of a Decomposable Stateless Deterministic STS Component . . . .
5.5.4 Correctness of Symbolic Feedback Composition . . . . . . . . . . . . . . . . . . . . . .
5.6 Closure Properties of MPT Subclasses w.r.t. Composition Operators . . . . . . . . . . . . . .
5.7 Symbolic Simplification of Arbitrary Composite Components . . . . . . . . . . . . . . . . . .
5.7.1 Deterministic and Algebraic Loop Free Composite Components . . . . . . . . . . . . .
5.7.2 Correctness of the Simplification Algorithm . . . . . . . . . . . . . . . . . . . . . . . .
5.8 Checking Validity and Compatibility . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
5.9 Checking Input-Receptiveness and Computing Legal Inputs Symbolically . . . . . . . . . . .
5.10 Checking Refinement Symbolically . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

25
25
26
27
27
28
28
28
28
28
28
29
30
30
30
30
30
30
30

6 Toolset and Case Studies

39

7 Related Work

41

2

31
31
31
31
31
32
32
33
34
36
37
37

8 Conclusion

1

43

Introduction

This paper presents the Refinement Calculus of Reactive Systems (RCRS), a comprehensive framework for
compositional modeling of and reasoning about reactive systems. RCRS originates from the precursor theory
of synchronous relational interfaces [78, 79], and builds upon the classic refinement calculus [10]. A number
of conference publications on RCRS exist [66, 31, 67, 65, 33]. This paper collects some of these results and
extends them in significant ways. The novel contributions of this paper and relation to our previous work
are presented in §1.1.
The motivation for RCRS stems from the need for a compositional treatment of reactive systems. Generally speaking, compositionality is a divide-and-conquer principle. As systems grow in size, they grow in
complexity. Therefore dealing with them in a monolithic manner becomes unmanageable. Compositionality
comes to the rescue, and takes many forms. Many industrial-strength systems have employed for many years
mechanisms for compositional modeling. An example is the Simulink tool from the Mathworks. Simulink is
based on the widespread notation of hierarchical block diagrams. Such diagrams are both intuitive, and naturally compositional: a block can be refined into sub-blocks, sub-sub-blocks, and so on, creating hierarchical
models of arbitrary depth. This allows the user to build large models (many thousands of blocks) while at
the same time managing their complexity (at any level of the hierarchy, only a few blocks may be visible).
But Simulink’s compositionality has limitations, despite its hierarchical modeling approach. Even relatively simple problems, such as the problem of modular code generation (generating code for a block
independently from context) require techniques not always available in standard code generators [53, 52].
Perhaps more serious, and more relevant in the context of this paper, is Simulink’s lack of formal semantics, and consequent lack of rigorous analysis techniques that can leverage the advances in the fields of
computer-aided verification and programming languages.
RCRS provides a compositional formal semantics for Simulink in particular, and hierarchical block diagram notations in general, by building on well-established principles from the formal methods and programming language domains. In particular, RCRS relies on the notion of refinement (and its counterpart,
abstraction) which are both fundamental in system design. Refinement is a binary relation between components, and ideally characterizes substitutability: the conditions under which some component can replace
another component, without compromising the behavior of the overall system. RCRS refinement is compositional in the sense that it is preserved by composition: if A0 refines A and B 0 refines B, then the composition
of A0 and B 0 refines the composition of A and B.
RCRS can be viewed as a refinement theory. It can also be viewed as a behavioral type system, similar to
type systems for programming languages, but targeted to reactive systems. By behavioral we mean a type
system that can capture not just data types of input and output ports of components (bool, int, etc.), but
also complete specifications of the behavior of those components. As discussed more extensively in [79], such
a behavioral type system has advantages over a full-blown verification system, as it is more lightweight: for
instance, it allows type checking, which does not require the user to provide a formal specification of the
properties that the model must satisfy, the model must simply type-check.
To achieve this, it is essential, as argued in [79], for the framework to be able to express non-inputreceptive (also called non-input-enabled or non-input-complete) components, i.e., components that reject
some input values. RCRS allows this. For example, a square-root component can be described√in RCRS
alternatively as: (1) a non-input-receptive component C1 with input-output contract x ≥ 0 ∧ y = x (where
x, y are the input
√ and output variables, respectively); or (2) an input-receptive component C2 with contract
x ≥ 0 → y = x. Simple examples of type-checking in the RCRS context are the following: Connecting the
non-input-receptive square-root component C1 to a component which outputs x = −1 results in a type error
(incompatibility). Connecting C1 to a non-deterministic component which outputs an arbitrary value for x
(this can be specified by the formula/contract true) also results in a type error. Yet, in both of the above
cases C2 will output a non-deterministically chosen value, even though the input constraint is not satisfied.
RCRS allows both non-input-receptive and non-deterministic components. This combination results in a
3

game-theoretic interpretation of the composition operators, like in interface theories [22, 79]. Refinement also
becomes game-theoretic, as in alternating refinement [7]. Game-theoretic composition can be used for an
interesting form of type inference. For example, if we connect the non-input-receptive square-root component
C1 above to a non-deterministic component C3 with input-output contract x ≥ u + 1 (where x is the output
of C3 , and u its input), and apply the (game-theoretic) serial composition of RCRS, we obtain the condition
u ≥ −1 on the external input of the overall composition. The constraint u ≥ −1 represents the weakest
condition on u which ensures compatibility of the connected components.
In a nutshell, RCRS consists of the following elements:
1. A modeling language (syntax), which allows to describe atomic components, and composite components
formed by a small number of primitive composition operators (serial, parallel, and feedback). The
language is described in §3.
2. A formal semantics, presented in §4. Component semantics are defined in terms of monotonic property
transformers (MPTs). MPTs are extensions of monotonic predicate transformers used in theories of
programming languages, and in particular in refinement calculus [10]. Predicate transformers transform
sets of post-states (states reached by the program after its computation) into sets of pre-states (states
where the program begins). Property transformers transform sets of a component’s output traces
(infinite sequences of output values) into sets of input traces (infinite sequences of input values). Using
this semantics we can express both safety and liveness properties.
3. A set of symbolic reasoning techniques, described in §5. In particular, RCRS offers techniques to
• compute the symbolic representation of a composite component from the symbolic representations
of its sub-components;
• simplify composite components into atomic components;
• reduce checking refinement between two components to checking satisfiability of certain logical
formulas;
• reduce input-receptiveness and compatibility checks to satisfiability;
• compute the legal inputs of a component symbolically.
We note that these techniques are for the most part logic-agnostic, in the sense that they do not depend
on the particular logic used to represent components.
4. A toolset, described briefly in §6. The toolset consists mainly of:
• a full implementation of the RCRS theory in the Isabelle proof assistant [61];
• a translator of Simulink diagrams into RCRS code.
Our implementation is open-source and publicly available from http://rcrs.cs.aalto.fi.

1.1

Novel contributions of this paper and relation to our prior work

Several of the ideas behind RCRS originated in the theory of synchronous relational interfaces [78, 79]. The
main novel contributions of RCRS w.r.t. that theory are: (1) RCRS is based on the semantic foundation
of monotonic property transformers, whereas relational interfaces are founded on relations; (2) RCRS can
handle liveness properties, whereas relational interfaces can only handle safety; (3) RCRS has been completely
formalized and most results reported in this and other RCRS papers have been proven in the Isabelle proof
assistant; (4) RCRS comes with a publicly available toolset (http://rcrs.cs.aalto.fi) which includes
the Isabelle formalization, a Translator of Simulink hierarchical block diagrams [31, 33], and a Formal
Analyzer which performs, among other functions, compatibility checking, refinement checking, and automatic
simplification of RCRS contracts.

4

RCRS was introduced in [66], which focuses on monotonic property transformers as a means to extend
relational interfaces with liveness properties. [66] covers serial composition, but not parallel nor feedback. It
also does not cover symbolic reasoning nor the RCRS implementation. Feedback is considered in [67], whose
aim is in particular to study instantaneous feedback for non-deterministic and non-input-receptive systems.
The study of instantaneous feedback is an interesting problem, but beyond the scope of the current paper.
In this paper we consider non-instantaneous feedback, i.e., feedback for systems without same-step cyclic
dependencies (no algebraic loops).
[31] presents part of the RCRS implementation, focusing on the translation of Simulink (and hierarchical
block diagrams in general) into an algebra of components with three composition primitives, serial, parallel,
and feedback, like RCRS. As it turns out, there is not a unique way to translate a graphical notation like
Simulink into an algebraic formalism like RCRS. The problem of how exactly to do it and what are the
trade-offs is an interesting one, but beyond the scope of the current paper. This problem is studied in
depth in [31] which proposes three different translation strategies and evaluates their pros and cons. [31]
leaves open the question whether the results obtained by the different translations are equivalent. [64] settles
this question, by proving that a class of translations, including the ones proposed in [31] are semantically
equivalent for any input block diagram. [65] also concerns the RCRS implementation, discussing solutions
to subtle typing problems that arise when translating Simulink diagrams into RCRS/Isabelle code.
In summary, the current paper does not cover the topics covered in [31, 64, 65, 67] and can be seen as a
significantly revised and extended version of [66]. The main novel contributions with respect to [66] are the
following: (1) a language of components (§3); (2) a revised MPT semantics (§4), including in particular novel
operators for feedback (§4.1.3) and a classification of MPT subclasses (§4.2); (3) a new section of symbolic
reasoning (§5).

2

Preliminaries

Sets, types. We use capital letters X, Y , Σ, . . . to denote types or sets, and small letters to denote
elements of these types x ∈ X, y ∈ Y , etc. We denote by B the type of Boolean values true and false. We
use ∧, ∨, ⇒, and ¬ for the Boolean operations. The type of natural numbers is denoted by N, while the
type of real numbers is denoted by R. The Unit type contains a single element denoted ().
Cartesian product. For types X and Y , X × Y is the Cartesian product of X and Y , and if x ∈ X and
y ∈ Y , then (x, y) is a tuple from X × Y . The empty Cartesian product is Unit. We assume that we have
only flat products X1 × . . . × Xn , and then we have
(X1 × . . . × Xn ) × (Y1 × . . . × Ym ) = X1 × . . . × Xn × Y1 × . . . × Ym
Functions. If X and Y are types, X → Y denotes the type of functions from X to Y . The function type
constructor associates to the right (e.g., X → Y → Z = X → (Y → Z)) and the function interpretation
associates to the left (e.g., f (x)(y) = (f (x))(y)). In order to construct functions we use lambda notation,
e.g., (λx, y : x + y + 1) : N → N → N. Similarly, we can have tuples in the definition of functions, e.g.,
(λ(x, y) : x + y + 2) : (N × N) → N. The composition of two functions f : X → Y and g : Y → Z, is a
function denoted g ◦ f : X → Z, where (g ◦ f )(x) = g(f (x)).
Predicates. A predicate is a function returning Boolean values, e.g., p : X → Y → B, p(x)(y) = (x = y).
We define the smallest predicate ⊥ : X → B where ⊥(x) = false for all x ∈ X. The greatest predicate is
> : X → B, with >(x) = true for all x ∈ X. We will often interpret predicates as sets. A predicate p : X → B
can be viewed as the set of all x ∈ X such that p(x) = true. For example, viewing two predicates p, q as sets,
we can write p ⊆ q, meaning that for all x, p(x) ⇒ q(x).

5

Relations. A relation is a predicate with at least two arguments, e.g., r : X → Y → B. For such a relation
r, we denote by in(r) : X → B the predicate in(r)(x) = (∃y : r(x)(y)). If the relation r has more than two
arguments, then we define in(r) similarly by quantifying over the last argument.
We extend point-wise all operations on Booleans to operations on predicates and relations. For example,
if r, r0 : X → Y → B are two relations, then r ∧ r0 and r ∨ r0 are the relations given by (r ∧ r0 )(x)(y) =
r(x)(y) ∧ r0 (x)(y) and (r ∨ r0 )(x)(y) = r(x)(y) ∨ r0 (x)(y). We also introduce the order on relations r ⊆ r0 =
(∀x, y : r(x)(y) ⇒ r0 (x)(y)).
The composition of two relations r : X → Y → B and r0 : Y → Z → B is a relation (r ◦ r0 ) : X → Z → B,
where (r ◦ r0 )(x)(z) = (∃y : r(x)(y) ∧ r0 (y)(z)).
Infinite sequences. If Σ is a type, then Σω = (N → Σ) is the set of all infinite sequences over Σ, also
called traces. For a trace σ ∈ Σω , let σi = σ(i) be the i-th element in the trace. Let σ i ∈ Σω denote the
suffix of σ starting from the i-th step, i.e., σ i = σi σi+1 · · · . We often view a pair of traces (σ, σ 0 ) ∈ Σω × Σ0ω
as being also a trace of pairs (λi : (σi , σi0 )) ∈ (Σ × Σ0 )ω .
Properties. A property is a predicate p over a set of infinite sequences. Formally, p ∈ (Σω → B). Just
like any other predicate, a property can also be viewed as a set. In particular, a property can be viewed as
a set of traces.

3

Language

3.1

An Algebra of Components

We model systems using a simple language of components. The grammar of the language is as follows:
component
atomic component
STS component

::=
::=
::=

composite component

::=

atomic component | composite component
STS component | QLTL component
GEN STS component | STATELESS STS component
| DET STS component | DET STATELESS STS component
component ; component | component k component | fdbk(component)

The elements of the above grammar are defined in the remaining of this section, where examples are
also given to illustrate the language. In a nutshell, the language contains atomic components of two kinds:
atomic components defined as symbolic transition systems (STS component), and atomic components defined
as QLTL formulas over input and output variables (QLTL component).
STS components are split in four categories: general STS components, stateless STS components, deterministic STS components, and deterministic stateless STS components. Semantically, the general STS
components subsume all the other more specialized STS components, but we introduce the specialized syntax
because symbolic compositions of less general components become simpler, as we shall explain in the sequel
(see §5).
Also, as it turns out, atomic components of our framework form a lattice, shown in Fig. 5, from the
more specialized ones, namely, deterministic stateless STS components, to the more general ones, namely
QLTL components. The full definition of this lattice will become apparent once we provide a symbolic
transformation of STS to QLTL components, in §5.1.
Apart from atomic components, the language also allows to form composite components, by composing
(atomic or other composite) components via three composition operators: serial ;, parallel k, and feedback
fdbk, as depicted in Fig. 1. The serial composition of two components C, C 0 is formed by connecting the
output(s) of C to the input(s) of C 0 . Their parallel composition is formed by “stacking” the two components
on top of each other without forming any new connections. The feedback of a component C is obtained by
connecting the first output of C to its first input.
Our language is inspired by graphical notations such as Simulink, and hierarchical block diagrams in
general. But our language is textual, not graphical. An interesting question is how to translate a graphical
6

x
x

y
C

y
C

0

z

u

(a) Serial composition: C ; C 0

y

x1

C
x2
..
.

v

C0

(b) Parallel composition: C k C 0

y1
C

y2
..
.

(c) Feedback composition: fdbk(C)

Figure 1: The three composition operators of RCRS.
block diagram into a term in our algebra. We will not address this question here, as the issue is quite
involved. We refer the reader to [31], which includes an extensive discussion on this topic. Suffice it to say
here that there are generally many possible translations of a graphical diagram into a term in our algebra (or
generally any algebra that contains primitive serial, parallel, and feedback composition operators). These
translations achieve different tradeoffs in terms of size, readability, computational properties, and so on.
See [31] for details.

1

1

In

z

Add

UnitDelay

1

Out

Figure 2: A Simulink diagram modeling the 1-step delayed sum of its input In. Each atomic block as well as
the entire system can be formalized as STS components (see §3.2). The entire system can also be formalized
as a composite component (see below).
As an example, consider the Simulink diagram shown in Fig. 2. This diagram can be represented in our
language as a composite component Sum defined as
Sum = fdbk(Add ; UnitDelay ; Split)
where Add, UnitDelay, and Split are atomic components (for a definition of these atomic components see
§3.2). Here Split models the “fan-out” element in the Simulink diagram (black bullet) where the output
wire of UnitDelay splits in two wires going to Out and back to Add.1

3.2

Symbolic Transition System Components

We introduce all four categories of STS components and at the same time provide syntactic mappings from
specialized STS components to general STS components.
3.2.1

General STS Components

A general symbolic transition system component (general STS component) is a transition system described
symbolically, with Boolean expressions over input, output, state, and next state variables defining the initial
states and the transition relation. When we say “Boolean expression” (here and in the definitions that
follow) we mean an expression of type B, in some arbitrary logic, not necessarily restricted to propositional
logic. For example, if x is a variable of numerical type, then x > 0 is a Boolean expression. In the definition
that follows, s0 denotes the primed, or next state variable, corresponding to the current state variable s. Both
1 Note that the Simulink input and output ports In and Out are not explicitly represented in Sum. They are represented
implicitly: In corresponds to the second input of Add, which carries over as the unique external input of Sum (thus, Sum is an
“open system” in the sense that it has open, unconnected, inputs); Out corresponds to the second output of Split, which carries
over as the unique external output of Sum.

7

can be vectors of variables. For example, if s = (s1 , s2 ) then s0 = (s01 , s02 ). We assume that s0 has the same
type as s.
Definition 1 (STS component). A (general) STS component is a tuple
sts(x : Σx , y : Σy , s : Σs , init exp : B, trs exp : B)
where x, y, s are input, output and state variables (or tuples of variables) of types Σx , Σy , Σs , respectively,
init exp is a Boolean expression on s (in some logic), and trs exp is a Boolean expression on x, y, s, s0 (in
some logic).
Intuitively, an STS component is a non-deterministic system which for an infinite input sequence σx ∈ Σω
x
produces as output an infinite sequence σy ∈ Σω
y . The system starts non-deterministically at some state
σs (0) satisfying init exp. Given first input σx (0), the system non-deterministically computes output σy (0)
and next state σs (1) such that trs exp holds (if no such values exist, then the input σx (0) is illegal, as
discussed in more detail below). Next, it uses the following input σx (1) and state σs (1) to compute σy (1)
and σs (2), and so on.
We will sometimes use the term contract to refer to the expression trs exp. Indeed, trs exp can be seen
as specifying a contract between the component and its environment, in the following sense. At each step in
the computation, the environment must provide input values that do not immediately violate the contract,
i.e., for which we can find values for the next state and output variables to satisfy trs exp. Then, it is the
responsibility of the component to find such values, otherwise it is the component’s “fault” if the contract
is violated. This game-theoretic interpretation is similar in spirit with the classic refinement calculus for
sequential programs [10].
We use Σx , Σy , Σs in the definition above to emphasize the types of the input, output and the state, and
the fact that, when composing components, the types should match. However, in practice we often omit the
types, unless they are required to unambiguously specify a component. Also note that the definition does not
fix the logic used for the expressions init exp and trs exp. Indeed, our theory and results are independent
from the choice of this logic. The choice of logic matters for algorithmic complexity and decidability. We
will return to this point in §5. Finally, for simplicity, we often view the formulas init exp and trs exp as
semantic objects, namely, as predicates. Adopting this view, init exp becomes the predicate init : Σs → B,
and trs exp the predicate trs exp : Σs → Σx → Σs → Σy → B. Equivalently, trs exp can be interpreted as
a relation trs exp : (Σs × Σx ) → (Σs × Σy ) → B.
Throughout this paper we assume that init exp is satisfiable, meaning that there is at least one valid
initial state.
Examples. In the examples provided in this paper, we often specify systems that have tuples as input,
state and output variables, in different equivalent ways. For example, we can introduce a general STS
component with two inputs as sts((n : N, x : R), s : R, y : R, s > 0, s0 > s ∧ y + s = xn ), but also as
sts((n, x) : N × R, s : R, y : R, s > 0, s0 > s ∧ y + s = xn ), or sts(z : N × R, y : R, s : R, s > 0, s0 > s ∧ y + s =
snd(z)fst(z) ), where fst and snd return the first and second elements of a pair.
Let us model a system that at every step i outputs the input received at previous step i − 1 (assume
that the initial output value is 0). This corresponds to Simulink’s commonly used UnitDelay block, which
is also modeled in the diagram of Fig. 2. This block can be represented by an STS component, where a state
variable s is needed to store the input at moment i such that it can be used at the next step. We formally
define this component as
UnitDelay = sts(x, y, s, s = 0, y = s ∧ s0 = x).
We use first-order logic to define init exp and trs exp. Here init exp is s = 0, which initializes the state
variable s with the value 0. The trs exp is y = s ∧ s0 = x, that is at moment i the current state variable s
which stores the input x received at moment i − 1 is outputed and its value is updated.
As another example, consider again the composite component Sum modeling the diagram of Fig. 2. Sum
could also be defined as an atomic STS component:
Sum = sts(x, y, s, s = 0, y = s ∧ s0 = s + x).
8

In §5 we will show how we can automatically and symbolically simplify composite component terms such
as fdbk(Add ; UnitDelay ; Split), to obtain syntactic representations of atomic components such as the one
above.
These examples illustrate systems coming from Simulink models. However, our language is more general,
and able to accommodate the description of other systems, such as state machines à la nuXmv [16], or
input/output automata [54]. In fact, both UnitDelay and Sum are deterministic, so they could also be
defined as deterministic STS components, as we will see below. Our language can capture non-deterministic
systems easily. An example of a non-deterministic STS component is the following:
C = sts(x, y, s, s = 0, x + s ≤ y).
For an input sequence σx ∈ Nω , C outputs a non-deterministically chosen sequence σy such that the transition
expression x + s ≤ y is satisfied. Since there is no formula in the transition expression tackling the next state
variable, this is updated also non-deterministically with values from N.
Our language can also capture non-input-receptive systems, that is, systems which disallow some input
values as illegal. For instance, a component performing division, but disallowing division by zero, can be
specified as follows:
x
Div = sts((x, y), z, (), true, y 6= 0 ∧ z = ).
y
Note that Div has an empty tuple of state variables, s = (). Such components are called stateless, and are
introduced in the sequel.
Even though RCRS is primarily a discrete-time framework, we have used it to model and verify continuoustime systems such as those modeled in Simulink (see §6). We do this by discretizing time using a time step
parameter ∆t > 0 and applying Euler numerical integration. Then, we can model Simulink’s Integrator
block in RCRS as an STS component parameterized by ∆t:

Integrator∆t

= sts x, y, s, s = 0, y = s ∧ s0 = s + x · ∆t



More complex dynamical system blocks can be modeled in a similar fashion. For instance, Simulink’s
Transfer Fcn block, with transfer function
s2 + 2
0.5s2 + 2s + 1
can be modeled in RCRS as the following STS component parameterized by ∆t:

TransferFcn∆t
where

= sts x, y, (s1 , s2 ), s1 = 0 ∧ s2 = 0, trs)

trs =

(y = −8 · s1 + 2 · x) ∧
(s01 = s1 + (−4 · s1 − 2 · s2 + x) · ∆t) ∧
(s02 = s2 + s1 · ∆t)

3.2.2

Variable Name Scope

We remark that variable names in the definition of atomic components are local. This holds for all atomic
components in the language of RCRS (including STS and QLTL components, defined in the sequel). This
means that if we replace a variable with another one in an atomic component, then we obtain a semantically equivalent component. For example, the two STS components below are equivalent (the semantical
equivalence symbol ≡ will be defined formally in Def. 20, once we define the semantics):
sts((x, y), z, s, s > 0, z > s + x + y) ≡ sts((u, v), w, t, t > 0, w > t + u + v)

9

3.2.3

Stateless STS Components

A special STS component is one that has no state variables:
Definition 2 (Stateless STS component). A stateless STS component is a tuple
C = stateless(x : Σx , y : Σy , io exp : B)
where x, y are the input and output variables, and io exp is a Boolean expression on x and y. Stateless STS
components are special cases of general STS components, as defined by the mapping stateless2sts:
stateless2sts(C) = sts(x, y, (), true, io exp).
Examples. A trivial stateless STS component is the one that simply transfers its input to its output (i.e.,
a “wire”). We denote such a component by Id, and we formalize it as
Id = stateless(x, y, y = x).
Another simple example is a component with no inputs and a single output, which always outputs a
constant value c (of some type). This can be formalized as the following component parameterized by c:
Constc = stateless((), y, y = c).
Component Add from Fig. 2, which outputs the sum of its two inputs, can be modeled as a stateless STS
component:
Add = stateless((x, y), z, z = x + y).
Component Split from Fig. 2 can also be modeled as a stateless STS component:
Split = stateless(x, (y, z), y = x ∧ z = x).
The Div component introduced above is stateless, and therefore can be also specified as follows:
x
.
Div = stateless (x, y), z, y 6= 0 ∧ z =
y
The above examples are not only stateless, but also deterministic. We introduce deterministic STS
components next.
3.2.4

Deterministic STS Components

Deterministic STS components are those which, for given current state and input, have at most one output
and next state. Syntactically, they are introduced as follows:
Definition 3 (Deterministic STS component). A deterministic STS component is a tuple
det(x : Σx , s : Σs , a : Σs , inpt exp : B, next exp : Σs , out exp : Σy )
where x, s are the input and state variables, a ∈ Σs is the initial value of the state variable, inpt exp is a
Boolean expression on s and x defining the legal inputs, next exp is an expression of type Σs on x and s
defining the next state, and out exp is an expression of type Σy on x and s defining the output. Deterministic
STS components are special cases of general STS components, as defined by the mapping det2sts:
det2sts(C) = (x, y, s, s = a, inpt exp ∧ s0 = next exp ∧ y = out exp)
where y is a new variable name (or tuple of new variable names) of type Σy .
Note that a deterministic STS component has a separate expression inpt exp to define legal inputs. A
separate such expression is not needed for general STS components, where the conditions for legal inputs
are part of the expression trs exp. For example, compare the definition of Div as a general STS above, and
as a stateless deterministic STS below (see §3.2.5).
10

Examples. As mentioned above, all three components, UnitDelay, Add, and Split from Fig. 2, as well as
Div and Const, are deterministic. They could therefore be specified in our language as deterministic STS
components, instead of general STS components:

UnitDelay = det x, s, 0, true, x, s

Constc = det (), (), (), true, (), c

Add = det (x, y), (), (), true, (), x + y

Split = det x, (), (), true, (), (x, x)
x
Div = det (x, y), (), (), y 6= 0, (),
y
The component Sum modeling the entire system is also deterministic, and could be defined as a deterministic STS component:
Sum = det(x, s, 0, true, s + x, s).
Note that these alternative specifications for each of those components, although syntactically distinct,
will turn out to be semantically equivalent by definition, when we introduce the semantics of our language,
in §4.
3.2.5

Stateless Deterministic STS Components

STS components which are both deterministic and stateless can be specified as follows:
Definition 4 (Stateless deterministic STS component). A stateless deterministic STS component is a tuple
C = stateless det(x : Σx , inpt exp : B, out exp : Σy )
where x is the input variable, inpt exp is a Boolean expression on x defining the legal inputs, and out exp is
an expression of type Σy on x defining the output. Stateless deterministic STS components are special cases
of both deterministic STS components, and of stateless STS components, as defined by the mappings
stateless det2det(C)

=

det(x, (), (), inpt exp, (), out exp)

stateless det2stateless(C)

=

stateless(x, y, inpt exp ∧ y = out exp)

where y is a new variable name or a tuple of new variable names.
Examples. Many of the examples introduced above are both deterministic and stateless. They could be
specified as follows:

Id
= stateless det x, true, x

Constc = stateless det (), true, c

Add
= stateless det (x, y), true, x + y

Split = stateless det x, true, (x, x)
x
Div
= stateless det (x, y), y 6= 0,
y

3.3

Quantified Linear Temporal Logic Components

Although powerful, STS components have limitations. In particular, they cannot express liveness properties [4]. To remedy this, we introduce another type of components, based on Linear Temporal Logic
(LTL) [63] and quantified propositional LTL (QPTL) [76, 48], which extends LTL with ∃ and ∀ quantifiers
over propositional variables. In this paper we use quantified first-order LTL (which we abbreviate as QLTL).
QLTL further extends QPTL with functional and relational symbols over arbitrary domains, quantification
11

of variables over these domains, and a next operator applied to variables.2 We need this expressive power
in order to be able to handle general models (e.g., Simulink) which often use complex arithmetic formulas,
and also to be able to translate STS components into semantically equivalent QLTL components (see §5.1).
3.3.1

QLTL

QLTL formulas are generated by the following grammar. We assume a set of constants and functional
symbols (0, 1, . . ., true, false, +, . . .), a set of predicate symbols (=, ≤, <, . . .), and a set of variable names
(x, y, z, . . .).
Definition 5 (Syntax of QLTL). A QLTL formula ϕ is defined by the following grammar:
term ::=

ϕ

::=

x | y | ... |
(variable names)
0 | 1 | . . . | true | . . . |
(constants)
term + term | . . . |
(functional symbol application)
# term
(next applied to a term)
term = term | (term ≤ term) | . . . | (atomic QLTL formulas)
¬ϕ |
(negation)
ϕ∨ψ |
(disjunction)
ϕUψ|
(until)
∀x : ϕ
(forall)

As in standard first order logic, the bounded variables of a formula ϕ are the variables in scope of the
universal quantifier ∀, and the free variables of ϕ are those that are not bounded. The logic connectives ∧,
⇒ and ⇔ can be expressed with ¬ and ∨. Quantification is over atomic variables. The existential quantifier
∃ can be defined via the universal quantifier usually as ¬∀¬. The primitive temporal operators are next for
terms (# ) and until ( U ). As is standard, QLTL formulas are evaluated over infinite traces, and ϕ U ψ
intuitively means that ϕ continuously holds until some point in the trace where ψ holds.
Formally, we will define the relation σ |= ϕ (σ satisfies ϕ) for a QLTL formula ϕ over free variables x, y, . . .,
and an infinite sequence σ ∈ Σω , where Σ = Σx × Σy × . . ., and Σx , Σy , . . . are the types (or domains) of
variables x, y, . . .. As before we assume that σ can be written as a tuple of sequences (σx , σy , . . .) where
ω
σ x ∈ Σω
x , σy ∈ Σy , . . .. The semantics of a term t on variables x, y, . . . is a function from infinite sequences
to infinite sequences hhtii : Σω → Σω
t , where Σ = Σx × Σy × . . ., and Σt is the type of t. When giving the
semantics of terms and formulas we assume that constants, functional symbols, and predicate symbols have
the standard semantics. For example, we assume that +, ≤, . . . on numeric values have the semantics of
standard arithmetic.
Definition 6 (Semantics of QLTL). Let x be a variable, t, t0 be terms, ϕ, ψ be QLTL formulas, P be a
predicate symbol, f be a functional symbol, c be a constant, and σ ∈ Σω be an infinite sequence.
hhxii(σ)
hhcii(σ)
hhf (t, t0 )ii(σ)
hh# tii(σ)
σ
σ
σ
σ
σ

|= P (t, t0 )
|= ¬ϕ
|= ϕ ∨ ψ
|= ϕ U ψ
|= (∀x : ϕ)

:= σx
:= (λi : c)
:= (λi : f (hhtii(σ)(i), hht0 ii(σ)(i)))
:= hhtii(σ 1 )
:=
:=
:=
:=
:=

P (hhtii(σ)(0), hht0 ii(σ)(0))
¬ σ |= ϕ
σ |= ϕ ∨ σ |= ψ
(∃n ≥ 0 : (∀ 0 ≤ i < n : σ i |= ϕ) ∧ σ n |= ψ)
(∀σx ∈ Σω
x : (σx , σ) |= ϕ)

Other temporal operators can be defined as follows. Eventually (F ϕ = true U ϕ) states that ϕ must
hold in some future step. Always (G ϕ = ¬F ¬ϕ) states that ϕ must hold at all steps. The next operator for
2 A logic similar to the one that we use here is presented in [47], however in [47] the next operator can be applied only once
to variables, and the logic from [47] uses also past temporal operators.

12

formulas X can be defined using the next operator for terms # . The formula X ϕ is obtained by replacing
all occurrences of the free variables in ϕ by their next versions (i.e., x is replaced by # x, y by # y, etc.).
For example the propositional LTL formula X (x ∧ X y ⇒ G z) can be expressed as
(# x = true ∧ (# # y = true) ⇒ G (# z = true)).

We additionally introduce the operator: ϕ L ψ := ¬(ϕ U ¬ψ). Intuitively, ϕ L ψ holds if whenever ϕ
holds continuously up to some step n − 1, ψ must hold at step n.
Two QLTL formulas ϕ and ψ are semantically equivalent, denoted ϕ ⇐⇒ ψ, if
∀σ : (σ |= ϕ) ⇐⇒ (σ |= ψ).
Lemma 1. Let ϕ be a QLTL formula. Then:
1. (∃x : G ϕ) ⇐⇒ G (∃x : ϕ) when ϕ does not contain temporal operators.
2. ϕ L ϕ ⇐⇒ G ϕ
3. true L ϕ ⇐⇒ G ϕ
4. ϕ L true ⇐⇒ true
5. ϕ L false ⇐⇒ false
6. ∀y : (ϕ L ψ) ⇐⇒ (∃y : ϕ) L ψ, when ϕ does not contain temporal operators and y is not free in ψ.
The proof of the above result, as well as of most results that follow, is omitted. All omitted proofs have
been formalized and proved in the Isabelle proof assistant, and are available as part of the public distribution
of RCRS from http://rcrs.cs.aalto.fi. In particular, all results contained in this paper can be accessed
from the theory RCRS Overview.thy – either directly in that file or via references to the other RCRS files.
Examples. Using QLTL we can express safety, as well as liveness requirements. Informally, a safety
requirement expresses that something bad never happens. An example is the formula
thermostat = G (180◦ ≤ t ∧ t ≤ 220◦ ),
which states that the thermostat-controlled temperature t stays always between 180◦ and 220◦ .
A liveness requirement informally says that something good eventually happens. An example is the
formula F (t > 200◦ ) stating that the temperature t is eventually over 200◦ .
A more complex example is a formula modeling an oven that starts increasing the temperature from an
initial value of 20◦ until it reaches 180◦ , and then keeps it between 180◦ and 220◦ .
oven = (t = 20◦ ∧ ((t < # t ∧ t < 180) U thermostat)).

In this example the formula t < # t specifies that the temperature increases from some point to the next.
3.3.2

QLTL Components

A QLTL component is an atomic component where the input-output behavior is specified by a QLTL formula:
Definition 7 (QLTL component). A QLTL component is a tuple qltl(x : Σx , y : Σy , ϕ), where x, y are
input and output variables (or tuples of variables) of types Σx , Σy , and ϕ is a QLTL formula over x and y.
Intuitively a QLTL component C = qltl(x, y, ϕ) represents a system that takes as input an infinite
ω
sequence σx ∈ Σω
x and produces as output an infinite sequence σy ∈ Σy such that (σx , σy ) |= ϕ. If there
is no σy such that (σx , σy ) |= ϕ is true, then input σx is illegal for C, i.e., C is not input-receptive. There
could be many possible σy for a single σx , in which case the system is non-deterministic.
As a simple example, we can model the oven as a QLTL component with no input variables and the
temperature as the only output variable:
qltl((), t, oven)
13

3.4

Well Formed Composite Components

Not all composite components generated by the grammar introduced in §3.1 are well formed. Two components C and C 0 can be composed in series only if the number of outputs of C matches the number of inputs
of C 0 , and in addition the input types of C 0 are the same as the corresponding output types of C. Also,
fdbk can be applied to a component C if the type of the first output of C is the same as the type of its first
input. Formally, for every component C we define below Σin (C) - the input type of C, Σout (C) - the output
type of C, and wf (C) - the well-formedness of C, by induction on the structure of C:
Σin (sts(x : Σx , y : Σy , s : Σs , init, trs))
Σin (stateless(x : Σx , y : Σy , trs))
Σin (det(x : Σx , s : Σs , a, inpt, next, out : Σy ))
Σin (stateless det(x : Σx , inpt, out : Σy ))
Σin (qltl(x : Σx , y : Σy , ϕ))
Σin (C ; C 0 )
Σin (C k C 0 )
Σin (fdbk(C))

Σout (sts(x : Σx , y : Σy , s : Σs , init, trs))
Σout (stateless(x : Σx , y : Σy , trs))
Σout (det(x : Σx , s : Σs , a, inpt, next, out : Σy ))
Σout (stateless det(x : Σx , inpt, out : Σy ))
Σout (qltl(x : Σx , y : Σy , ϕ))
Σout (C ; C 0 )
Σout (C k C 0 )
Σout (fdbk(C))

wf (sts(x, y, s, init, trs))
=
wf (stateless(x, y, trs))
=
wf (det(x, s, a, inpt, next, out))
=
wf (stateless det(x, inpt, out)) =
wf (qltl(x, y, ϕ))
=
wf (C ; C 0 )
=
wf (C k C 0 )
=
wf (fdbk(C))
=

=
=
=
=
=
=
=
=

=
=
=
=
=
=
=
=

Σx
Σx
Σx
Σx
Σx
Σin (C)
Σin (C) × Σin (C 0 )
X2 × · · · × Xn provided Σin (C) = X1 × · · · × Xn
for some n ≥ 1

Σy
Σy
Σy
Σy
Σy
Σout (C 0 )
Σout (C) × Σout (C 0 )
Y2 × · · · × Yn provided Σout (C) = Y1 × · · · × Yn
for some n ≥ 1

true
true
true
true
true
wf (C) ∧ wf (C 0 ) ∧ Σout (C) = Σin (C 0 )
wf (C) ∧ wf (C 0 )
wf (C) ∧ Σin (C) = X × X1 · · · × Xn
∧ Σout (C) = X × Y1 · · · × Ym , for some n, m ≥ 0.

In the definition above, both n and m are natural numbers. If n = 0 then X1 × · · · × Xn denotes the Unit
type.
Note that atomic components are by definition well-formed. The composite components considered in
the sequel are required to be well-formed too.
We note that the above well-formedness conditions are not restrictive. Components that do not have
matching inputs and outputs can still be composed by adding appropriate switching components which
reorder inputs, duplicate inputs, and so on. An example of such a component is the component Split,
introduced earlier. As another example, consider the diagram in Fig. 3:
This diagram can be expressed in our language as the composite component:
A ; Switch1 ; (B k Id) ; Switch2 ; (C k Id)

14

A

B

C

Figure 3: Another block diagram.
where
Switch1 = stateless det((x, y), true, (x, y, x))
Switch2 = stateless det((u, v, x), true, (u, x, v))

4

Semantics

In RCRS, the semantics of components is defined in terms of monotonic property transformers (MPTs).
This is inspired by classical refinement calculus [10], where the semantics of sequential programs is defined in
terms of monotonic predicate transformers [28]. Predicate transformers are functions that transform sets of
post-states (states reached after the program executes) into sets of pre-states (states from which the program
begins). Property transformers map sets of output traces (that a component produces) into sets of input
traces (that a component consumes).
In this section we define MPTs formally, and introduce some basic operations on them, which are necessary for giving the semantics of components. The definitions of some of these operations (e.g., product
and fusion) are simple extensions of the corresponding operations on predicate transformers [10, 9]. Other
operations, in particular those related to feedback, are new (§4.1.3). The definition of component semantics
is also new (§4.3).

4.1

Monotonic Property Transformers

ω
A property transformer is a function S : (Σω
y → B) → (Σx → B), where Σx , Σy are input and output types
of the component in question. Note that x is the input and y is the output. A property transformer has
a weakest precondition interpretation: it is applied to a set of output traces Q ⊆ Σω
y , and returns a set of
,
such
that
all
traces
in
P
are
legal
and,
when
fed
to
the
component,
are guaranteed to
input traces P ⊆ Σω
x
produce only traces in Q as output.
Interpreting properties as sets, monotonicity of property transformers simply means that these functions
are monotonic with respect to set inclusion. That is, S is monotonic if for any two properties q, q 0 , if q ⊆ q 0
then S(q) ⊆ S(q 0 ).
For an MPT S we define its set of legal input traces as legal(S) = S(>), where > is the greatest predicate
extended to traces. Note that, because of monotonicity, and the fact that q ⊆ > holds for any property q,
we have that S(q) ⊆ legal(S) for all q. This justifies the definition of legal(S) as a “maximal” set of input
traces for which a system does not fail, assuming no restrictions on the post-condition. An MPT S is said
to be input-receptive if legal(S) = >.

4.1.1

Some Commonly Used MPTs

Definition 8 (Skip). Skip is defined to be the MPT such that for all q, Skip(q) = q.
Skip models the identity function, i.e., the system that accepts all input traces and simply transfers them
unchanged to the output (this will become more clear when we express Skip in terms of assert or update
transformers, below). Note that Skip is different from Id, defined above, although the two are strongly
related: Id is a component, i.e., a syntactic object, while Skip is an MPT, i.e., a semantic object. As we
shall see in §4.3, the semantics of Id is defined as Skip.
Definition 9 (Fail). Fail is defined to be the MPT such that for all q, Fail(q) = ⊥.
15

Recall that ⊥ is the predicate that returns false for any input. Thus, viewed as a set, ⊥ is the empty set.
Consequently, Fail can be seen to model a system which rejects all inputs, i.e., a system such that for any
output property q, there are no input traces that can produce an output trace in q.
Definition 10 (Assert). Let p ∈ Σω → B be a property. The assert property transformer {p} : (Σω → B) →
(Σω → B) is defined by
{p}(q) = p ∧ q.
The assert transformer {p} can be seen as modeling a system which accepts all input traces that satisfy
p, and rejects all others. For all the traces that it accepts, the system simply transfers them, i.e., it behaves
as the identity function.
To express MPTs such as assert transformers syntactically, let us introduce some notation. First, we can
use lambda notation for predicates, as in λ(σ, σ 0 ) : (σ = σ 0 ) for some predicate p : Σω → Σω → B which
returns true whenever it receives two equal traces. Then, instead of writing {λ(σ, σ 0 ) : (σ = σ 0 )} for the
corresponding assert transformer {p}, we will use the slightly lighter notation {σ, σ 0 | σ = σ 0 }.
ω
Definition 11 (Demonic update). Let r : Σω
x → Σy → B be a relation. The demonic update property
ω
ω
transformer [r] : (Σy → B) → (Σx → B) is defined by

[r](q) = {σ | ∀σ 0 : r(σ)(σ 0 ) ⇒ σ 0 ∈ q}.
That is, [r](q) contains all input traces σ which are guaranteed to result into an output trace in q when
fed into the (generally non-deterministic) input-output relation r. The term “demonic update” comes from
the refinement calculus literature [10].
Similarly to assert, we introduce a lightweight notation for the demonic update. If r is an expression in σ
and σ 0 , then [σ ; σ 0 | r] = [λ(σ, σ 0 ) : r]. For example, [σx , σy ; σz | ∀i : σz (i) = σx (i) + σy (i)] is the system
which produces as output the sequence σz = (λi : σx (i) + σy (i)), where σx and σy are the input sequences.
If e is an expression in σ, then [σ ; e] is defined to be [σ ; σ 0 | σ 0 = e], where σ 0 is a new variable different
from σ and which does not occur free in e. For example, [σ ; (λi : σ(i) + 1)] = [σ ; σ 0 | σ 0 = (λi : σ(i) + 1)].
The following lemma states that Skip can be defined as an assert transformer, or as a demonic update
transformer.
Lemma 2. Skip = [σ ; σ 0 | σ = σ 0 ] = {>} = {σ | true}.

In general Skip, Fail, and other property transformers are polymorphic with respect to their input and
output types. In Skip the input and output types must be the same. Fail, on the other hand, may have an
input type and a different output type.
ω
Definition 12 (Angelic update). Let r : Σω
x → Σy → B be a relation. The angelic update property
ω
ω
transformer {r} : (Σy → B) → (Σx → B) is defined by

{r}(q) = {σ | ∃σ 0 : r(σ)(σ 0 ) ∧ σ 0 ∈ q}.
An input sequence σ is in {r}(q) if there exists an output sequence σ 0 such that r(σ)(σ 0 ) and σ 0 ∈ q.
Notice the duality between the angelic and demonic update transformers. Consider, for example, a relation
r = {(σ, σ 0 ), (σ, σ 00 )}. If q = {σ 0 , σ 00 }, then {r}(q) = [r](q) = {σ}. If q = {σ 0 } then {r}(q) = {σ}, while
[r](q) = ∅.
We use a lightweight notation for the angelic update transformer, similar to the one for demonic update.
If r is an expression in σ and σ 0 , then {σ ; σ 0 | r} = {λ(σ, σ 0 ) : r}.
Lemma 3. Assert is a particular case of angelic update: {p} = {σ ; σ 0 | p(σ) ∧ σ = σ 0 }.

16

4.1.2

Operators on MPTs: Function Composition, Product, and Fusion

As we shall see in §4.3, the semantics of composition operators in the language of components will be defined
by the corresponding composition operators on MPTs. We now introduce the latter operators on MPTs.
First, we begin by the operators that have been known in the literature, and are recalled here. In §4.1.3 we
introduce some novel operators explicitly designed in order to handle feedback composition.
Serial composition of MPTs (and property transformers in general) is simply function composition. Let
ω
ω
ω
S : (Σω
y → B) → (Σx → B) and T : (Σz → B) → (Σy → B) be two property transformers. Then
ω
ω
S ◦ T : (Σz → B) → (Σx → B), is the function composition of S and T , i.e., ∀q : (S ◦ T )(q) = S(T (q)). Note
that serial composition preserves monotonicity, so that if S and T are MPTs, then S ◦ T is also an MPT.
Also note that Skip is the neutral element for serial composition, i.e., S ◦ Skip = Skip ◦ S = S.
To express parallel composition of components, we need a kind of Cartesian product operation on property
transformers. We define such an operation below. Similar operations for predicate transformers have been
proposed in [9].
ω
ω
ω
Definition 13 (Product). Let S : (Σω
y → B) → (Σx → B) and T : (Σv → B) → (Σu → B). The product of
ω
ω
ω
ω
S and T , denoted S ⊗ T : (Σy × Σv → B) → (Σx × Σu → B), is given by
0
ω
0
0
0
(S ⊗ T )(q) = {(σ, σ 0 ) | ∃p : Σω
y → B, p : Σv → B : p × p ⊆ q ∧ σ ∈ S(p) ∧ σ ∈ T (p )}

where (p × p0 )(σy , σv ) = p(σy ) ∧ p0 (σv ).
Lemma 4. For arbitrary S and T , S ⊗ T is monotonic.
The neutral element for the product composition is the Skip MPT that has Unit as input and output
type.
In order to define a feedback operation on MPTs, we first define two auxiliary operations: Fusion and
IterateOmega. Fusion is an extension of a similar operator introduced previously for predicate transformers
in [9]. IterateOmega is a novel operator introduced in the sequel.
ω
Definition 14 (Fusion). If S = {Si }i∈I , Si : (Σω
y → B) → (Σx → B) is a collection of MPTs, then the
ω
ω
fusion of S is the MPT Fusioni∈I (Si ) : (Σy → B) → (Σx → B) defined by
\
\
(Fusioni∈I (Si ))(q) = {σ | ∃p : I → Σω
pi ⊆ q ∧ σ ∈
Si (pi )}
y →B:
i

i

The Fusion operator satisfies the following property.
Lemma 5. For I 6= ∅ we have
Fusioni∈I ({pi } ◦ [ri ]) = {

\

i∈I

4.1.3

pi } ◦ [

\

ri ].

i∈I

Novel Operators Used in Semantical Definition of Feedback

The IterateOmega operator is defined as follows:
Definition 15 (IterateOmega).
IterateOmega(S) = Fusionn∈N (S n ◦ [σ ; σ 0 | ∀i : i + 1 < n ⇒ σi = σi0 ])

The feedback operator consists of connecting the first output of an MPT S with its first input. Formally,
feedback is defined as follows.
ω
Definition 16 (Feedback). Let S : (Σu × Σω
y → B) → (Σu × Σx → B) be an MPT. The feedback operator
on S, denoted Feedback(S), is given by the MPT

Feedback(S)

=

{σx ; σu , σy , σx }
◦ IterateOmega([σu , σy , σx ; σu , σx , σx ] ◦ (S ⊗ Skip))
◦ [σu , σy , σx ; σy ]
17

Example. As an example we show how to derive Feedback(S) for S = [σu , σx ; 0 · σx + 0 · σu , 0 · σx + 0 · σu ],
where σ + σ 0 = (λi : σ(i) + σ 0 (i)), and 0 · σ is 0 concatenated with σ. For now, we note that S is the semantics
of the composite component Add ; UnitDelay ; Split, which corresponds to the inner part of the diagram of
Fig. 2, before applying feedback. We will complete the formal definition of the the semantics of this diagram
in §4.3. For now, we focus on deriving Feedback(S), in order to illustrate how the Feedback operator works.
Let
T = [σu , σy , σx ; σu , σx , σx ] ◦ (S ⊗ Skip) = [σu , σy , σx ; 0 · σx + 0 · σu , 0 · σx + 0 · σu , σx ]

Then, we have
T ◦T
...
Tn

=
=

[σu , σy , σx ; 0 · σx + 0 · 0 · σx + 0 · 0 · σu , 0 · σx + 0 · 0 · σx + 0 · 0 · σu , σx ]

[σu , σy , σx ; 0 · σx + . . . + 0n · σx + 0n · σu , 0 · σx + . . . + 0n · σx + 0n · σu , σx ]

where 0n is a finite sequence of n 0s. We also have
=

T n ◦ [σ ; σ 0 | ∀i : i + 1 < n ⇒ σi = σi0 ]

[σu , σy , σx ; σ | ∀i : i + 1 < n ⇒ σ(i) = (Σj<i σx (j), Σj<i σx (j), σx (i))]

Then
Feedback(S)
=
=
=
=

{σx ; σu , σy , σx } ◦ IterateOmega(T ) ◦ [σu , σy , σx ; σy ]

{σx ; σu , σy , σx } ◦ Fusionn∈N (T n ◦ [σ ; σ 0 | ∀i : i + 1 < n ⇒ σi = σi0 ]) ◦ [σu , σy , σx ; σy ]

{σx ; σu , σy , σx } ◦ [σu , σy , σx ; σ | ∀i : σ(i) = (Σj<i σx (j), Σj<i σx (j), σx (i))] ◦ [σu , σy , σx ; σy ]
[σx ; σy | ∀i : σy (i) = Σj<i σx (j)]

Finally we obtain

Feedback(S) = [σx ; σy | ∀i : σy (i) = Σj<i σx (j)]

(1)

This is the system that outputs the trace (λi : Σj<i σx (j)) for input trace σx .
4.1.4

Refinement

A key element of RCRS, as of other compositional frameworks, is the notion of refinement, which enables
substitutability and other important concepts of compositionality. Semantically, refinement is defined as
follows:
ω
Definition 17 (Refinement). Let S, T : (Σω
y → B) → (Σx → B) be two MPTs. We say that T refines S (or
that S is refined by T ), written S v T , if and only if ∀q : S(q) ⊆ T (q).

All operations introduced on MPTs preserve the refinement relation:
Theorem 1. If S, T, S 0 , T 0 are MPTs of appropriate types such that S v S 0 and T v T 0 , then
1. S ◦ T v S 0 ◦ T 0 and S ⊗ T v S 0 ⊗ T 0 and Fusion(S, T ) v Fusion(S 0 , T 0 ) ([9, 10])
2. IterateOmega(S) v IterateOmega(S 0 )
3. Feedback(S) v Feedback(S 0 )

18

4.2

Subclasses of MPTs

Monotonic property transformers are a very rich and powerful class of semantic objects. In practice, the
systems that we deal with often fall into restricted subclasses of MPTs, which are easier to represent syntactically and manipulate symbolically. We introduce these subclasses next.
4.2.1

Relational MPTs

Definition 18 (Relational property transformers). A relational property transformer (RPT) S is an MPT
of the form {p} ◦ [r]. We call p the precondition of S and r the input-output relation of S.
Relational property T
transformers
T correspond to conjunctive transformers [10]. A transformer S is conjunctive if it satisfies S( i∈I qi ) = i∈I S(qi ) for all (qi )i∈I and I 6= ∅.
Fail, Skip, any assert transformer {p}, and any demonic update transformer [r], are RPTs. Indeed, Fail
can be written as {σ | false} ◦ [σ ; σ 0 | true]. Skip can be written as {σ | true} ◦ [σ ; σ]. The assert
transformer {p} can be written as the RPT {p} ◦ [σ ; σ]. Finally, the demonic update transformer [r] can
be written as the RPT {σ | true} ◦ [r]. Angelic update transformers are generally not RPTs: the angelic
update transformer {σ ; σ 0 | true} is not an RPT, as it is not conjunctive.
Examples. Suppose we wish to specify a system that performs division. Here are two possible ways to
represent this system with RPTs:
S1 = {>} ◦ [σx , σy ; σz | ∀i : σy (i) 6= 0 ∧ σz (i) =

σx (i)
]
σy (i)

S2 = {σx , σy | ∀i : σy (i) 6= 0} ◦ [σx , σy ; σz | σz (i) =

σx (i)
]
σy (i)

Although S1 and S2 are both relational, they are not equivalent transformers. S1 is input-receptive: it accepts
all input traces. However, if at some step i the input σy (i) is 0, then the output σz (i) is arbitrary (nondeterministic). In contrast, S2 is non-input-receptive as it accepts only those traces σy that are guaranteed
to be non-zero at every step, i.e., those that satisfy the condition ∀i : σy (i) 6= 0.
Theorem 2 (RPTs are closed under serial, product and fusion compositions). Let S = {p} ◦ [r] and
S 0 = {p0 } ◦ [r0 ] be two RPTs, with p, p0 , r and r0 of appropriate types. Then
S ◦ S 0 = {σ | p(σ) ∧ (∀σ 0 : r(σ)(σ 0 ) ⇒ p0 (σ 0 ))} ◦ [r ◦ r0 ]
and
and

S ⊗ S 0 = {σx , σy | p(σx ) ∧ p0 (σy )} ◦ [σx , σy ; σx0 , σy0 | r(σx )(σx0 ) ∧ r0 (σy )(σy0 )]
Fusion(S, S 0 ) = {p ∧ p0 } ◦ [r ∧ r0 ]

RPTs are not closed under Feedback. For example, we have
Feedback([σx , σz ; σx , σx ]) = {σ ; σ 0 | true}

which is a non-relational angelic update transformer as we said above.
Next theorem shows that the refinement of RPTs can be reduced to proving a first order property.
Theorem 3. For p, p0 , r, r0 of appropriate types we have.
{p} ◦ [r] v {p0 } ◦ [r0 ] ⇐⇒ (p ⊆ p0 ∧ (∀σx : p(σx ) ⇒ r0 (σx ) ⊆ r(σx )))

19

4.2.2

Guarded MPTs

Relational property transformers correspond to systems that have natural syntactic representations, as the
composition {p} ◦ [r], where the predicate p and the relation r can be represented syntactically in some
logic. Unfortunately, RPTs are still too powerful. In particular, they allow system semantics that cannot
be implemented. For example, consider the RPT Magic = [σ ; σ 0 | false]. It can be shown that for any
output property q (including ⊥), we have Magic(q) = >. Recall that, viewed as a set, > is the set of all
traces. This means that, no matter what the post-condition q is, Magic somehow manages to produce output
traces satisfying q no matter what the input trace is (hence the name “magic”). In general, an MPT S is
said to be non-miraculous (or to satisfy the law of excluded miracle) if S(⊥) = ⊥. We note that in [28],
sequential programs are modeled using predicate transformers that are conjunctive and satisfy the low of
excluded miracle.
We want to further restrict RPTs so that miraculous behaviour does not arise. Specifically, for an RPT
S = {p} ◦ [r] and an input sequence σ, if there is no σ 0 such that r(σ)(σ 0 ) is satisfied, then we want σ to be
illegal, i.e., we want p(σ) = false. We can achieve this by taking p to be in(r). Recall that if r : X → Y → B,
then in(r)(x) = (∃y : r(x)(y)). Taking p to be in(r) effectively means that p and r are combined into a
single specification r which can also restrict the inputs. This is also the approach followed in the theory of
relational interfaces [79].
Definition 19 (Guarded property transformers). The guarded property transformer (GPT) of a relation r
is an RPT, denoted {r], defined by {r] = {in(r)} ◦ [r].
It can be shown that an MPT S is a GPT if and only if S is conjunctive and non-miraculous [10]. Fail,
Skip, and any assert property transformer are GPTs. Indeed, Fail = {⊥] and Skip = {σ ; σ | >]. The
assert transformer can be written as {p} = {σ ; σ | p(σ)]. The angelic and demonic update property
transformers are generally not GPTs. The angelic update property transformer is not always conjunctive in
order to be a GPT. The demonic update property transformer is not in general a GPT because is not always
non-miraculous (Magic(⊥) = > =
6 ⊥). The demonic update transformer [r] is a GPT if and only if in(r) = >
and in this case we have [r] = {r].
Theorem 4 (GPTs are closed under serial and parallel compositions). Let S = {r] and S 0 = {r0 ] be two
GPTs with r and r0 of appropriate types. Then

S ◦ S 0 = {σx ; σz | in(r)(σx ) ∧ ∀σy : r(σx )(σy ) ⇒ in(r0 )(σy ) ∧ (r ◦ r0 )(σx , σz )]
and

S ⊗ S 0 = {σx , σy ; σx0 , σy0 | r(σx )(σx0 ) ∧ r0 (σy )(σy0 )]

GPTs are not closed under Fusion neither Feedback. Indeed, we have already seen in the previous section
that Feedback applied to the GPT [σx , σz ; σx , σx ] is not an RPT, and therefore not a GPT either. For the
fusion operator, we have Fusion([x ; 0], [x ; 1]) = [⊥], which is not a GPT.
A corollary of Theorem 3 is that refinement of GPTs can be checked as follows:
Corollary 1.
{r] v {r0 ] ⇐⇒ (in(r) ⊆ in(r0 ) ∧ (∀σx : in(r)(σx ) ⇒ r0 (σx ) ⊆ r(σx )))
4.2.3

Other subclasses and overview

The containment relationships among the various subclasses of MPTs are illustrated in Fig. 4. In addition
to the subclasses discussed above, we introduce several more subclasses of MPTs in the sections that follow,
when we assign semantics (in terms of MPTs) to the various atomic components in our component language.
For instance, QLTL components give rise to QLTL property transformers. Similarly, STS components,
stateless STS components, etc., give rise to corresponding subclasses of MPTs. The containment relationships
between these classes will be proven in the sections that follow. For ease of reference, we provide some forward
links to these results also here. The fact that QLTL property transformers are GPTs follows by definition
20

of the semantics of QLTL components: see §4.3, equation (2). The fact that STS property transformers are
a special case of QLTL property transformers follows from the transformation of an STS component into a
semantically equivalent QLTL component: see §5.1 and Theorem 7. The inclusions for subclasses of STS
property transformers follow by definition of the corresponding components (see also Fig. 5).
Monotonic Property Transformers
Relational Property Transformers
Guarded Property Transformers
QLTL Property Transformers
STS Property Transformers
Stateless STS Property Transformers
Deterministic STS Property Transformers

Figure 4: Overview of the property transformer classes and their containment relations.

4.3

Semantics of Components as MPTs

We are now ready to define the semantics of our language of components in terms of MPTs. Let C be a well
formed component. The semantics of C, denoted [[C]], is a property transformer of the form:
[[C]] : ((Σout (C))ω → B) → ((Σin (C))ω → B).
We define [[C]] by induction on the structure of C. First we give the semantics of QLTL components and
composite components:
[[qltl(x, y, ϕ)]]
0

=

{σx ; σy | (σx , σy ) |= ϕ]

(2)

0

[[C ; C ]]

=

[[C]] ◦ [[C ]]

(3)

[[C k C 0 ]]

=

[[C]] ⊗ [[C 0 ]]

(4)

[[fdbk(C)]]

=

Feedback([[C]])

(5)

The semantics of QLTL components satisfies the following property:
Lemma 6. If ϕ is a LTL formula on variables x and y, we have:
[[qltl(x, y, (∃y : ϕ) ∧ ϕ)]] = [[qltl(x, y, ϕ)]]
To define the semantics of STS components, we first introduce some auxiliary notation.
ω
Consider an STS component C = sts(x, y, s, init exp, trs exp). We define the predicate runC : Σω
s × Σx ×
ω
Σy → B as
runC (σs , σx , σy ) = (∀i : trs exp(σs (i), σx (i))(σs (i + 1), σy (i))).
ω
ω
Intuitively, if σx ∈ Σω
x is the input sequence, σy ∈ Σy is the output sequence, and σs ∈ Σs is the sequence
of values of state variables, then runC (σs , σx , σy ) holds if at each step of the execution, the current state,
current input, next state, and current output, satisfy the trs exp predicate.

21

We also formalize the illegal input traces of STS component C as follows:
illegalC (σx ) = (∃σs , σy , k : init exp(σs (0)) ∧ (∀i < k : trs exp(σs (i), σx (i))(σs (i + 1), σy (i))) ∧
¬in(trs exp)(σs (k), σx (k)))
Essentially, illegalC (σx ) states that there exists some point in the execution where the current state and
current input violate the precondition in(trs exp) of predicate trs exp, i.e., there exist no output and next
state to satisfy trs exp for that given current state and input.
Then, the semantics of an STS component C is given by:
[[C]] = {¬illegalC } ◦ [σx ; σy | (∃σs : init exp(σs (0)) ∧ runC (σs , σx , σy ))]

(6)

We give semantics to stateless and/or deterministic STS components using the corresponding mappings
from general STS components. If C is a stateless STS, C 0 is a deterministic STS, and C 00 is a stateless
deterministic STS, then:

[[C]]
0

[[C ]]
00

[[C ]]

=
=
=

[[stateless2sts(C)]]

(7)

0

[[det2sts(C )]]

(8)
00

[[stateless det2det(C )]]

(9)

Note that the semantics of a stateless deterministic STS component C 00 is defined by converting C 00 into
a deterministic STS component, by Equation (9) above. Alternatively, we could have defined the semantics
of C 00 by converting it into a stateless STS component, using the mapping stateless det2stateless. In
order for our semantics to be well-defined, we need to show that regardless of which conversion we choose,
we obtain the same result. Indeed, this is shown by the lemma that follows:
Lemma 7. For a stateless deterministic STS C 00 we have:
[[stateless det2det(C 00 )]] = [[stateless det2stateless(C 00 )]]

(10)

Observe that, by definition, the semantics of QLTL components are GPTs. The semantics of STS
components are defined as RPTs. However, they will be shown to be GPTs in §5.1. Therefore, the semantics
of all atomic RCRS components are GPTs. This fact, and the closure of GPTs w.r.t. parallel and serial
composition (Theorem 4), ensure that we stay within the GPT realm as long as no feedback operations are
used. In addition, as we shall prove in Corollary 2, components with feedback are also GPTs, as long as
they are deterministic and do not contain algebraic loops. An example of a component whose semantics is
not a GPT is:
C = fdbk(stateless((x, z), (y1 , y2 ), y1 = x ∧ y2 = x))
Then, we have [[C]] = Feedback([σx , σz ; σx , σx ]). As stated earlier, Feedback([σx , σz ; σx , σx ]) is equal to
{σ ; σ 0 | true}, which is not a GPT neither an RPT. The problem with C is that it contains an algebraic
loop: the first output y1 of the internal stateless component where feedback is applied directly depends on
its first input x. Dealing with such components is beyond the scope of this paper, and we refer the reader
to [67].
4.3.1

Example: Two Alternative Derivations of the Semantics of Diagram Sum of Fig. 2

To illustrate our semantics, we provide two alternative derivations of the semantics of the Sum system of
Fig. 2.
First, let us consider Sum as a composite component:
Sum = fdbk(Add ; UnitDelay ; Split)

22

where
Add
=
UnitDelay =
Split
=

stateless det((u, x), true, u + x)
det(x, s, 0, true, x, s)
stateless det(x, true, (x, x))

We have
[[Sum]]

= [[fdbk(Add ; UnitDelay ; Split)]]
= Feedback([[Add]] ◦ [[UnitDelay]] ◦ [[Split]])

For Add, UnitDelay and Split, all inputs are legal,
After simplifications, we get:
[[Add]]
=
[[UnitDelay]] =
[[Split]]
=
The semantics of Sum is given by

so illegalC = ⊥ for all C ∈ {Add, UnitDelay, Split}.
[σu , σx ; σu + σx ]
[σx ; 0 · σx ]
[σx ; σx , σx ]

[[Sum]]
=
Feedback([[Add]] ◦ [[UnitDelay]] ◦ [[Split]]
=
=
=

We obtain:

Feedback([σu , σx ; σu + σx ] ◦ [σx ; 0 · σx ] ◦ [σx ; σx , σx ])
Feedback([σu , σx ; 0 · σx + 0 · σu , 0 · σx + 0 · σu ])
{Using (1)}

[σx ; σy | ∀i : σy (i) = Σj<i σx (j)]
[[Sum]] = [σx ; σy | ∀i : σy (i) = Σj<i σx (j)].

Next, let us assume that the system has been characterized already as an atomic component:
SumAtomic = sts(x, y, s, s = 0, y = s ∧ s0 = s + x).
The semantics of SumAtomic is given by
[[SumAtomic]] = {¬illegalSumAtomic } ◦ [σx ; σy | ∃σs : σs (0) = 0 ∧ runSumAtomic (σs , σx , σy )]

where illegalSumAtomic = ⊥ because there are no restrictions on the inputs of SumAtomic, and

runSumAtomic (σs , σx , σy ) = ∀i : σy (i) = σs (i) ∧ σs (i + 1) = σs (i) + σx (i)
We have


[[SumAtomic]] = [σx ; σy | ∃σs : σs (0) = 0 ∧ ∀i : σy (i) = σs (i) ∧ σs (i + 1) = σs (i) + σx (i) ]

which is equivalent to (11).
4.3.2

Characterization of Legal Input Traces

The following lemma characterizes legal input traces for various types of MPTs:
Lemma 8. The set of legal input traces of an RPT {p} ◦ [r] is p:
legal({p} ◦ [r]) = p.

23

(11)

The set of legal input traces of a GPT {r] is in(r):
legal({r]) = in(r).
The set of legal input traces of an STS component C = sts(x, y, s, init, r) is equal to ¬illegalC :
legal([[C]]) = ¬illegalC .
The set of legal input traces of a QLTL component C = qltl(x, y, ϕ) is:
legal([[C]]) = {σx | σx |= ∃y : ϕ}.
4.3.3

Semantic Equivalence and Refinement for Components

Definition 20. Two components C and C 0 are (semantically) equivalent, denoted C ≡ C 0 , if [[C]] = [[C 0 ]].
Component C is refined by component C 0 , denoted C  C 0 , if [[C]] v [[C 0 ]].
The relation ≡ is an equivalence relation, and  is a preorder relation (i.e., reflexive and transitive). We
also have
(C  C 0 ∧ C 0  C) ⇐⇒ (C ≡ C 0 )
4.3.4

Compositionality Properties

Several desirable compositionality properties follow from our semantics:
Theorem 5. Let C1 , C2 , C3 , and C4 be four (possibly composite) components. Then:
1. (Serial composition is associative:) (C1 ; C2 ) ; C3 ≡ C1 ; (C2 ; C3 ).
2. (Parallel composition is associative:) (C1 k C2 ) k C3 ≡ C1 k (C2 k C3 ).
3. (Parallel composition distributes over serial composition:) If [[C1 ]] and [[C2 ]] are GPTs and [[C3 ]] and
[[C4 ]] are RPTs, then (C1 k C2 ) ; (C3 k C4 ) ≡ (C1 ; C3 ) k (C2 ; C4 ).
4. (Refinement is preserved by composition:) If C1  C2 and C3  C4 , then:
(a) C1 ; C3  C2 ; C4
(b) C1 k C3  C2 k C4
(c) fdbk(C1 )  fdbk(C2 )
In addition to the above, requirements that a component satisfies are preserved by refinement. Informally,
if C satisfies some requirement ϕ and C  C 0 then C 0 also satisfies ϕ. Although we have not formally defined
what requirements are and what it means for a component to satisfy a requirement, these concepts are
naturally captured in the RCRS framework via the semantics of components as MPTs. In particular, since
our components are generally open systems (i.e., they have inputs), we can express requirements using Hoare
triples of the form p{C}q, where C is a component, p is an input property, and q is an output property. Then,
p{C}q holds iff the outputs of C are guaranteed to satisfy q provided the inputs of C satisfy p. Formally:
p{C}q ⇐⇒ p ⊆ [[C]](q).
Theorem 6. C  C 0 iff ∀p, q : p{C}q ⇒ p{C 0 }q.
Theorem 6 shows that refinement is equivalent to substitutability. Substitutability states that a component
C 0 can replace another component C in any context, i.e., ∀p, q : p{C}q ⇒ p{C 0 }q.

24

5

Symbolic Reasoning

So far we have defined the syntax and semantics of RCRS. These already allow us to specify and reason about
systems in a compositional manner. However, such reasoning is difficult to do “by hand”. For example, if
we want to check whether a component C is refined by another component C 0 , we must resort to proving
the refinement relation [[C]] v [[C 0 ]] of their corresponding MPTs, [[C]] and [[C 0 ]]. This is not an easy task,
as MPTs are complex mathematical objects. Instead, we would like to have computer-aided, and ideally
fully automatic techniques. In the above example of checking refinement, for instance, we would like ideally
to have an algorithm that takes as input the syntactic descriptions of C and C 0 and replies yes/no based
on whether [[C]] v [[C 0 ]] holds. We say “ideally” because we know that in general such an algorithm cannot
exist. This is because we are not making a-priori any restrictions on the logics used to describe C and C 0 ,
which means that the existence of an algorithm will depend on decidability of these logics. In this section,
we describe how reasoning in RCRS can be done symbolically, by automatically manipulating the formulas
used to specify the components involved. As we shall show, most problems can be reduced to checking
satisfiability of first-order formulas formed by combinations of the formulas of the original components. This
means that the problems are decidable whenever the corresponding first-order logics are decidable.

5.1

Symbolic Transformation of STS Components to QLTL Components

Our framework allows the specification of several types of atomic components, some of which are special
cases of others, as summarized in Fig. 5. In §3, we have already shown how the different types of STS
components are related, from the most specialized deterministic stateless STS components, to the general
STS components. By definition, the semantics of the special types of STS components is defined via the
semantics of general STS components (see §4). In this subsection, we show that STS components can be
viewed as special cases of QLTL components.
qltl
sts
stateless

det

stateless det
Figure 5: Lattice of atomic components: lower types are special cases of higher types.
Specifically, we show how an STS component can be transformed into a semantically equivalent QLTL
component. This transformation also shows that STS property transformers are a special case of QLTL
property transformers, as already claimed in Fig. 4. Note that this containment is not obvious simply by
looking at the definitions of these MPT subclasses (c.f. §4.3), as QLTL property transformers are defined as
GPTs (equation 2), whereas STS property transformers are defined as RPTs (equation 6). Although RPTs
are generally a superclass, not a subclass, of GPTs, the transformation proposed below shows that the RPTs
obtained from STS components can indeed be captured as GPTs. The transformation of STS into QLTL
components also enables us to apply several algorithms which are available for QLTL components to STS
components as well.
Consider an STS component C = sts(x, y, s, init, trs). We can transform C into a QLTL component
using the mapping sts2qltl:
sts2qltl(C) = qltl(x, y, (∀s, y : init ⇒ (ϕ L ϕ0 )) ∧ (∃s : init ∧ G ϕ))
where ϕ = trs[s0 := # s] and ϕ0 = (∃s0 , y : trs).
The theorem that follows demonstrates the correctness of the above transformation:
25

(12)

Theorem 7. For any STS component C = sts(x, y, s, init, trs) s.t. init is satisfiable, C ≡ sts2qltl(C).
Example. It is instructive to see how the above transformation specializes to some special types of STS
components. In particular, we will show how it specializes to stateless STS components.
Let C = stateless(x, y, trs) and let C 0 = stateless2sts(C) = sts(x, y, (), true, trs). Applying the
sts2qltl transformation to C 0 , for which s = () and init = true, we obtain:

sts2qltl(C 0 ) = qltl x, y, (∀y : (ϕ L ϕ0 )) ∧ G ϕ)
where ϕ = trs[() := # ()] = trs and ϕ0 = (∃y : trs). Using the properties of Lemma 1, and the fact that
semantically equivalent LTL formulas result in semantically equivalent QLTL components, we can simplify
sts2qltl(C 0 ) further:
sts2qltl(C 0 )
= {Definition of sts2qltl}

qltl x, y, (∀y : (trs L (∃y : trs))) ∧ G trs
≡

{Lemma 1, trs does not contain temporal operators, and y is not free in (∃y : trs)}

qltl x, y, ((∃y : trs) L (∃y : trs)) ∧ G trs

≡

{Lemma 1}

qltl x, y, G (∃y : trs) ∧ G trs

≡

{Lemma 1 and trs does not contain temporal operators}

qltl x, y, (∃y : G trs) ∧ G trs

≡

{Lemma 6}

qltl x, y, G trs

Note that in the above derivation we use the equivalence symbol ≡, in addition to the equality symbol =.
Recall that ≡ stands for semantical equivalence of two components (c.f. §4.3.3). On the other hand, = for
components means syntactic equality. By definition of the semantics, if two QLTL formulas are equivalent,
then the corresponding QLTL components are equivalent.
Based on the above, we define the transformation stateless2qltl of a stateless component C =
stateless(x, y, trs), into a QLTL component as follows:

stateless2qltl(C) = qltl x, y, G trs

5.2

Symbolic Transformations of Special Atomic Components to More General
Atomic Components

Based on the lattice in Fig. 5, we define all remaining mappings from more special atomic components to more
general atomic components, by composing the previously defined mappings sts2qltl, stateless2qltl,
stateless2sts, det2sts, stateless det2stateless and stateless det2det, as appropriately.
For mapping stateless deterministic STS components to QLTL components, we have two possibilities:
stateless det → det → sts → qltl and stateless det → stateless → qltl. We choose the transformation stateless det → stateless → qltl because it results in a simpler formula:
stateless det2qltl(C) = stateless2qltl(stateless det2stateless(C)).
Examples.

Consider the following STS components:
C1
C2
UnitDelay


= stateless x, y, y > x

= stateless x, (), x > 0

= det x, s, 0, true, x, s
26

Then:


stateless2qltl(C1 )

= qltl x, y, G y > x

stateless2qltl(C2 )

= qltl x, (), G x > 0

det2qltl(UnitDelay)



= qltl x, y, (∀s, y : s = 0 ⇒
(true ∧ # s = x ∧ y = s) L (∃s0 , y : true ∧ s0 = x ∧ y = s)) ∧

(∃s : s = 0 ∧ G (true ∧ # s = x ∧ y = s))

Because (∃s0 , y : true ∧ s0 = x ∧ y = s)) ⇐⇒ true, using Lemma 1 and logical simplifications we obtain:

det2qltl(UnitDelay) ≡ qltl x, y, (∃s : s = 0 ∧ G (# s = x ∧ y = s))

≡ qltl x, y, (∃s : s = 0 ∧ G (# y = x ∧ y = s))

≡ qltl x, y, (∃s : s = 0 ∧ G (y = s) ∧ G (# y = x))

≡ qltl x, y, (∃s : y = 0 ∧ G (y = s) ∧ G (# y = x))

≡ qltl x, y, (∃s : G (y = s)) ∧ y = 0 ∧ G (# y = x)

≡ qltl x, y, G (∃s : y = s) ∧ y = 0 ∧ G (# y = x)

≡ qltl x, y, y = 0 ∧ G (# y = x)

5.3

Symbolic Computation of Serial Composition

Given a composite component C formed as the serial composition of two components C1 and C2 , i.e.,
C = C1 ; C2 , we would like to compute a new, atomic component Ca , such that Ca is semantically equivalent
to C. Because atomic components are by definition represented syntactically (and symbolically), being able
to reduce composite components into atomic components means that we are able to symbolically compute
composition operators.
We start by defining the symbolic serial composition of components of the same type.
5.3.1

Symbolic Serial Composition of Two QLTL Components

Let C = qltl(x, y, ϕ) and C 0 = qltl(y, z, ϕ0 ) such that C ; C 0 is well formed. Then their symbolic serial
composition, denoted serial(C, C 0 ), is the QLTL component defined by

serial(C, C 0 ) = qltl x, z, (∀y : ϕ ⇒ (∃z : ϕ0 )) ∧ (∃y : ϕ ∧ ϕ0 )

(13)

Note that in the above definition (as well as the ones that follow) we assume that the output variable
of C and the input variable of C 0 have the same name (y) and that the names x, y and z are distinct. In
general, this may not be the case. This is not a problem, as we can always rename variables such that this
condition is met. Note that variable renaming does not change the semantics of components (c.f. §3.2.2).
The intuition behind the formula in (13) is as follows. The second conjunct ∃y : ϕ ∧ ϕ0 ensures that
the both contracts ϕ and ϕ0 of the two components are enforced in the composite contract. The reason
we use ∃y : ϕ ∧ ϕ0 instead of just the conjunction ϕ ∧ ϕ0 is that we want to eliminate (“hide”) internal
variable y. (Alternatively, we could also have chosen to output y as an additional output, but would then
need an additional hiding operator to remove y.) The first conjunct ∀y : ϕ ⇒ (∃z : ϕ0 ) is a formula on
the input variable x of the composite component (since all other variables y and z are quantified). This
formula restricts the legal inputs of C to those inputs for which, no matter which output C produces, this
output is guaranteed to be a legal input for the downstream component C 0 . For an extensive discussion of
the intuition and justification behind this definition, see [79].

27

5.3.2

Symbolic Serial Composition of Two General STS Components

Let C = sts(x, y, s, init, trs) and C 0 = sts(y, z, t, init0 , trs0 ) be two general STS components such that
C ; C 0 is well formed. Then:

serial(C, C 0 ) = sts x, z, (s, t), init∧init0 , (∃s0 , y : trs)∧(∀s0 , y : trs ⇒ (∃t0 , z : trs0 ))∧(∃y : trs∧trs0 ) (14)
5.3.3

Symbolic Serial Composition of Two Stateless STS Components

Let C = stateless(x, y, trs) and C 0 = stateless(y, z, trs0 ) be two stateless STS components such that
C ; C 0 is well formed. Then

serial(C, C 0 ) = stateless x, z, (∀y : trs ⇒ (∃z : trs0 )) ∧ (∃y : trs ∧ trs0 )
(15)
5.3.4

Symbolic Serial Composition of Two Deterministic STS Components

Let C = det(x, s, a, p, next, out) and C 0 = det(y, t, b, p0 , next0 , out0 ) be two deterministic STS components
such that their serial composition C ; C 0 is well formed. Then:
serial(C, C 0 ) = det(x, (s, t), (a, b), p ∧ p0 [y := out], (next, next0 [y := out]), out0 [y := out])

(16)

where e[z := e0 ] denotes the substitution of all free occurences of variable z by expression e0 in expression e.
5.3.5

Symbolic Serial Composition of Two Stateless Deterministic STS Components

Finally, let C = stateless det(x, p, out) and C 0 = stateless det(y, p0 , out0 ) be two stateless deterministic
STS components such that their serial composition C ; C 0 is well formed. Then:
serial(C, C 0 ) = stateless det(x, p ∧ p0 [y := out], out0 [y := out])
5.3.6

(17)

Symbolic Serial Composition of Two Arbitrary Atomic Components

In general, we define the symbolic serial composition of two atomic components C and C 0 by using the
mappings of less general components to more general components (Fig. 5), as appropriate. For example, if C is a deterministic STS component and C 0 is a stateless STS component, then serial(C, C 0 ) =
serial(det2sts(C), stateless2sts(C 0 )). Similarly, if C is a QLTL component and C 0 is a deterministic STS component, then serial(C, C 0 ) = serial(C, det2qltl(C 0 )). Formally, assume that atm, atm 0 ∈
{qltl, sts, stateless, det, stateless det} are the types of the components C and C 0 , and common =
atm ∨ atm 0 is the least general component type that is more general than atm and atm 0 as defined in Fig. 5.
Then
serial(C, C 0 ) = serial(atm2common(C), atm 0 2common(C 0 )).
5.3.7

Correctness of Symbolic Serial Composition

The following theorem demonstrates that our symbolic computations of serial composition are correct, i.e.,
that the resulting atomic component serial(C, C 0 ) is semantically equivalent to the original composite component C ; C 0 :
Theorem 8. If C and C 0 are two atomic components, then
C ; C 0 ≡ serial(C, C 0 ).

28

Examples.

Consider the following STS components:
C1

= stateless(u, (x, y), true)

C2

x
= stateless det((x, y), y 6= 0, )
y

Then:
serial(C1 , C2 )

= serial(C1 , stateless det2stateless(C2 ))
= serial(stateless(u, (x, y), true), stateless((x, y), z, y 6= 0 ∧ z =
= stateless(u, z, (∀x, y : true ⇒ (∃z : y 6= 0 ∧ z =
∧ (∃x, y : true ∧ y 6= 0 ∧ z =

x
))
y

x
))
y

x
)))
y

≡ stateless(u, z, false)
As we can see, the composition results in a stateless STS component with input-output formula false. The
semantics of such a component is Fail, indicating that C1 and C2 are incompatible. Indeed, in the case of
C1 ; C2 , the issue is that C2 requires its second input, y, to be non-zero, but C1 cannot guarantee that. The
reason is that the input-output formula of C1 is true, meaning that, no matter what its input u is, C1 may
output any value for x and y, non-deterministically. This violates the input requirements of C2 , causing
an incompatibility. We will return to this point in §5.8. We also note that this type of incompatibility is
impossible to prevent, by controlling the input u. In the example that follows, we see a case where the two
components are not incompatible, because the input requirements of the downstream component can be met
by strengthening the input assumptions of the upstream component:
Consider the following QLTL components:
C3

= qltl(x, y, G (x ⇒ F y))

C4

= qltl(y, (), G F y)

Then:
serial(C3 , C4 )

= serial(qltl(x, y, G (x ⇒ F y)), qltl(y, (), G F y))
= qltl(x, (), (∀y : (G (x ⇒ F y)) ⇒ G F y) ∧ (∃y : G (x ⇒ F y) ∧ G F y))
≡ qltl(x, (), G F x)

In this example, the downstream component C4 requires its input y to be infinitely often true (G F y).
This can be achieved only if the input x of the upstream component is infinitely often true, which is the
condition derived by the serial composition of C3 and C4 (G F x). Notice that C3 does not impose any apriori requirements on its input. However, its input-output relation is the so-called request-response property
which can be expressed as: whenever the input x is true, the output y will eventually become true afterwards
(G (x ⇒ F y)). This request-response property implies that in order for y to be infinitely-often true, x must
be infinitely-often true. Moreover, this is the weakest possible condition that can be enforced on x in order
to guarantee that the condition on y holds.

5.4

Symbolic Computation of Parallel Composition

Given a composite component formed as the parallel composition of two components, C = C1 k C2 , we
would like to compute an atomic component Ca , such that Ca is semantically equivalent to C. We show
how this can be done in this subsection. The symbolic computation of parallel composition follows the same
pattern as the one for serial composition (§5.3).

29

5.4.1

Symbolic Parallel Composition of Two QLTL Components

Let C = qltl(x, y, ϕ) and C 0 = qltl(u, v, ϕ0 ).
parallel(C, C 0 ), is the QLTL component defined by

Then their symbolic parallel composition, denoted

parallel(C, C 0 ) = qltl (x, u), (y, v), ϕ ∧ ϕ0



(18)

As in the case of symbolic serial composition, we assume that variable names x, y, u, v are all distinct. If
this is not the case, then we rename variables as appropriately.
5.4.2

Symbolic Parallel Composition of Two General STS Components

Let C = sts(x, y, s, init, trs) and C 0 = sts(u, v, t, init0 , trs0 ). Then:
parallel(C, C 0 ) = sts (x, u), (y, v), (s, t), init ∧ init0 , trs ∧ trs0
5.4.3



(19)

Symbolic Parallel Composition of Two Stateless STS Components

Let C = stateless(x, y, trs) and C 0 = stateless(u, v, trs0 ). Then
parallel(C, C 0 ) = stateless (x, u), (y, v), trs ∧ trs0
5.4.4



(20)

Symbolic Parallel Composition of Two Deterministic STS Components

Let C = det(x, s, a, p, next, out) and C 0 = det(u, t, b, p0 , next0 , out0 ). Then:

parallel(C, C 0 ) = det (x, u), (s, t), (a, b), p ∧ p0 , (next, next0 ), (out, out0 )
5.4.5

(21)

Symbolic Parallel Composition of Two Stateless Deterministic STS Components

Let C = stateless det(x, p, out) and C 0 = stateless det(u, p0 , out0 ). Then:
parallel(C, C 0 ) = stateless det (x, u), p ∧ p0 , (out, out0 )
5.4.6



(22)

Symbolic Parallel Composition of Two Arbitrary Atomic Components

Similar to the symbolic serial composition, we define the symbolic parallel composition of two atomic components C and C 0 by using the mappings of less general components to more general components (Fig. 5), as
appropriate. Formally, assume that atm, atm 0 ∈ {qltl, sts, stateless, det, stateless det} are the types
of the components C and C 0 , and common = atm ∨ atm 0 is the least general component type that is more
general than atm and atm 0 as defined in Fig. 5. Then
parallel(C, C 0 ) = parallel(atm2common(C), atm 0 2common(C 0 )).
5.4.7

Correctness of Symbolic Parallel Composition

The following theorem demonstrates that our symbolic computations of parallel composition are also correct,
i.e., that the resulting atomic component parallel(C, C 0 ) is semantically equivalent to the original composite
component C k C 0 :
Theorem 9. If C and C 0 are two atomic components, then
C k C 0 ≡ parallel(C, C 0 ).

30

5.5
5.5.1

Symbolic Computation of Feedback Composition for Decomposable Deterministic STS Components
Decomposable Components

We provide a symbolic closed-form expression for the feedback composition of a deterministic STS component, provided such a component is decomposable. Intuitively, decomposability captures the fact that the
first output of the component, y1 , does not depend on its first input, x1 . This ensures that the feedback
composition (which connects y1 to x1 ) does not introduce any circular dependencies.
Definition
21
(Decomposability).
Let
C
be
a
deterministic
STS

det (x1 , . . . , xn ), s, a, p, next, (e1 , . . . , em )  or
a
stateless
deterministic
STS
stateless det (x1 , . . . , xn ), p, (e1 , . . . , em ) . C is called decomposable if x1 is not free in e1 .

component
component

e1
x1
x2 , . . . , x n

•

e2
...
em

e1
x2 , . . . , x n

(a)

•

x1

e2
...
em

(b)

Figure 6: (a) Decomposable deterministic component; (b) the same component after applying feedback,
connecting its first output to x1 .
Decomposability is illustrated in Fig. 6a. The figure shows that expression e1 depends only on inputs
x2 , . . . , x n .
5.5.2

Symbolic Feedback of a Decomposable Deterministic STS Component

For a decomposable deterministic STS component C = det((x1 , . . . , xn ), s, a, p, next, (e1 , . . . , em )), its symbolic feedback composition, denoted feedback(C), is the deterministic STS component defined by

feedback(C) = det (x2 , . . . , xn ), s, a, p[x1 := e1 ], next[x1 := e1 ], (e2 [x1 := e1 ], . . . , em [x1 := e1 ])
(23)
Thus, computing feedback symbolically consists in removing the first input of the component and replacing
the corresponding variable x1 by the expression of the first output, e1 , everywhere where x1 appears. The
feedback operator is illustrated in Fig. 6b.
5.5.3

Symbolic Feedback of a Decomposable Stateless Deterministic STS Component

For a decomposable stateless deterministic STS component C = stateless det((x1 , . . . , xn ), p, (e1 , . . . , em )),
feedback(C) is the stateless deterministic STS component defined by

feedback(C) = stateless det (x2 , . . . , xn ), p[x1 := e1 ], (e2 [x1 := e1 ], . . . , em [x1 := e1 ])
(24)
5.5.4

Correctness of Symbolic Feedback Composition

Theorem 10. If C is a decomposable deterministic STS component, then
fdbk(C) ≡ feedback(C)

31

Providing closed-form symbolic computations of feedback composition for general components, including
possibly non-deterministic STS and QLTL components, is an open problem, beyond the scope of the current
paper. We remark that the straightforward idea of adding to the contract the equality constraint x = y
where y is the output connected in feedback to input x, does not work.3
In fact, even obtaining a semantically consistent compositional definition of feedback for non-deterministic
and non-input-receptive systems is a challenging problem [67]. Nevertheless, the results that we provide here
are sufficient to cover the majority of cases in practice. In particular, the symbolic operator feedback can
be used to handle Simulink diagrams, provided these diagrams do not contain algebraic loops, i.e., circular
dependencies (see §5.7).

5.6

Closure Properties of MPT Subclasses w.r.t. Composition Operators

In addition to providing symbolic computation procedures, the results of the above subsections also prove
closure properties of the various MPT subclasses of RCRS with respect to the three composition operators.
These closure properties are summarized in Tables 1 and 2.
In a nutshell, both serial and parallel composition preserve the most general type of the composed
components, according to the lattice in Fig. 5. For instance, the serial (or parallel) composition of two
stateless STS components is a stateless STS component; the serial (or parallel) composition of a stateless
STS component and a general STS component is a general STS component; and so on. Feedback preserves
the type of its component (deterministic or stateless deterministic).
; and k
qltl
sts
stateless
det
stateless det

qltl
qltl
qltl
qltl
qltl
qltl

sts
qltl
sts
sts
sts
sts

stateless
qltl
sts
stateless
sts
stateless

det
qltl
sts
sts
det
det

stateless det
qltl
sts
stateless
det
stateless det

Table 1: Closure properties of serial and parallel compositions. The table is to be read as follows: given
atomic components C1 , C2 of types as specified in a row/column pair, the serial or parallel composition of
C1 and C2 is an atomic component of type as specified in the corresponding table entry.

fdbk

det and decomposable
det

stateless det and decomposable
stateless det

Table 2: Closure properties of feedback composition.

5.7

Symbolic Simplification of Arbitrary Composite Components

The results of the previous subsections show how to simplify into an atomic component the serial or parallel
composition of two atomic components, or the feedback composition of an atomic decomposable component. We can combine these techniques in order to provide a general symbolic simplification algorithm: the
algorithm takes as input an arbitrarily complex composite component, and returns an equivalent atomic
component. The algorithm is shown in Fig. 7.
The algorithm fails only in case it encounters the feedback of a non-decomposable component. Recall
that decomposability implies determinism (c.f. §5.5.1), which means that the test C 00 is decomposable means
3 One of several problems of this definition is that it does not preserve refinement. For example, the stateless component
with contract x 6= y refines the stateless component with contract true. Adding the constraint x = y to both contracts yields
the components with contracts x = y and false, respectively, where the latter no longer refines the former. For a more detailed
discussion, see [67].

32

atomic(C) :
if C is atomic then
return C
else if C is C 0 ; C 00 then
return serial(atomic(C 0 ), atomic(C 00 ))
else if C is C 0 k C 00 then
return parallel(atomic(C 0 ), atomic(C 00 ))
else if C is fdbk(C 0 ) then
C 00 := atomic(C 0 )
if C 00 is decomposable then
return feedback(C 00 )
else
fail
else /* impossible by definition of syntax */
fail
Figure 7: Simplification algorithm for arbitrary composite components.
that C 00 is of the form det((x1 , . . .), s, a, p, next, (e1 , . . .)) or stateless det((x1 , . . .), p, (e1 , . . .)) and x1 is
not free in e1 .
We note that in practice, our RCRS implementation on top of Isabelle performs more simplifications in
addition to those performed by the procedure atomic. For instance, our implementation may be able to
simplify a logical formula φ into an equivalent but simpler formula φ0 (e.g., by eliminating quantifiers from
φ), and consequently also simplify a component, say, qltl(x, y, φ) into an equivalent but simpler component
qltl(x, y, φ0 ). These simplifications very much depend on the logic used in the components. Describing the
simplifications that our implementation performs is outside the scope of the current paper, as it belongs in
the realm of computational logic. It suffices to say that our tool is not optimized for this purpose, and could
leverage specialized tools and relevant advances in the field of computational logic.
5.7.1

Deterministic and Algebraic Loop Free Composite Components

In order to state and prove correctness of the algorithm, we extend the notion of determinism to a composite
component. We also introduce the notion of algebraic loop free components, which capture systems with no
circular and intantaneous input-output dependencies.
A (possibly composite) component C is said to be deterministic if every atomic component of C is either
a deterministic STS component or a stateless deterministic STS component. Formally, C is deterministic iff
determ(C) is true, where determ(C) is defined inductively on the structure of C:
determ(det(x, s, a, p, n, e))
=
determ(stateless det(x, p, e)) =
determ(sts(x, y, s, init, trs))
=
determ(stateless(x, y, trs))
=
determ(C ; C 0 )
=
determ(C k C 0 )
=
determ(fdbk(C))
=

true
true
false
false
determ(C) ∧ determ(C 0 )
determ(C) ∧ determ(C 0 )
determ(C)

Notice that this notion of determinism applies to a generally composite component C, i.e., a syntactic term
in our algebra of components, involving atomic components possibly composed via the three composition operators. This notion of determinism is the generalization of the syntactically deterministic STS components,
33

which are atomic. This notion of determinism is also distinct from any semantic notion of determinism
(which we have not introduced at all in this paper, as it is not needed).
For a deterministic component we define its output input dependency relation. Let C be deterministic,
and let Σin (C) = X1 × . . . × Xn and Σout (C) = Y1 × . . . × Ym . The relation OI(C) ⊆ {1, . . . , m} × {1, . . . , n}
is defined inductively on the structure of C:
OI(det((x1 , . . . , xn ), s, a, p, next, (e1 , . . . , em )))
=
OI(stateless det((x1 , . . . , xn ), p, (e1 , . . . , em ))) =
OI(C ; C 0 )
=
OI(C k C 0 )
=

OI(fdbk(C))

=

{(i, j) | xj is free in ei }
{(i, j) | xj is free in ei }
OI(C 0 ) ◦ OI(C)
OI(C) ∪ {(i + m, j + n) | (i, j) ∈ OI(C 0 )}
where Σin (C) = X1 × . . . × Xn
and Σout (C) = Y1 × . . . × Ym
{(i, j) | i > 0 ∧ j > 0 ∧ ((i + 1, j + 1) ∈ OI(C)
∨ ((i + 1, 1) ∈ OI(C) ∧ (1, j + 1) ∈ OI(C)))}

The intuition is that (i, j) ∈ OI(C) iff the i-th output of C depends on its j-th input.
The OI relation is preserved by the symbolic operations, as shown by the following lemma:
Lemma 9. If C and C 0 are deterministic STS components, then
OI(C ; C 0 )
OI(C k C 0 )

= OI(serial(C, C 0 ))
= OI(parallel(C, C 0 )).

If C is also decomposable, then
OI(fdbk(C))

= OI(feedback(C)).

We introduce now the the notion of algebraic loop free component. Intuitively, a (possibly composite)
deterministic component C is algebraic loop free if, whenever C contains a subterm of the form fdbk(C 0 ),
the first output of C 0 does not depend on its first input. This implies that whenever a feedback connection
is formed, no circular dependency is introduced. It also ensures that the simplification algorithm will never
fail. Formally, for a component C such that determ(C) is true, loop-free(C) is defined inductively on the
structure of C:
loop-free(C)
=
loop-free(C)
=
loop-free(C ; C 0 )
=
loop-free(C k C 0 )
=
loop-free(fdbk(C)) =
5.7.2

true if C = det(x, s, a, p, next, out)
true if C = stateless det(x, p, out)
loop-free(C) ∧ loop-free(C 0 )
loop-free(C) ∧ loop-free(C 0 )
loop-free(C) ∧ (1, 1) 6∈ OI(C)

Correctness of the Simplification Algorithm

Theorem 11. Let C be a (possibly composite) component.
1. If C does not contain any fdbk operators then atomic(C) does not fail and returns an atomic component such that atomic(C) ≡ C.
2. If determ(C) ∧ loop-free(C) is true then atomic(C) does not fail and returns an atomic component
such that atomic(C) ≡ C. Moreover, atomic(C) is a deterministic STS component and
OI(C) = OI(atomic(C)).
Proof. The first part of the theorem is a consequence of the fact that the symbolic serial and parallel
compositions are defined for all atomic components and return equivalent atomic components, by Theorems 8
and 9.
34

For the second part, since we have a recursive procedure, we prove its correctness by asumming the
correctness of the recursive calls. Additionally, the termination of this procedure is ensured by the fact
that all recursive calls are made on “smaller” components. Specifically: we assume that both determ(C)
and loop-free(C) hold; and we prove that atomic(C) does not fail, atomic(C) is a deterministic STS
component, atomic(C) ≡ C, and OI(C) = OI(atomic(C)).
We only consider the case C = fdbk(C 0 ). All other cases are similar, but simpler. Because determ(C)
and loop-free(C) hold, we have that determ(C 0 ) and loop-free(C 0 ) also hold, and in addition (1, 1) 6∈
OI(C 0 ). Using the correctness assumption for the recursive call we have that atomic(C 0 ) does not fail,
C 00 = atomic(C 0 ) is a deterministic STS component, C 00 ≡ C 0 , and OI(C 00 ) = OI(C 0 ).
Because C 00 is a deterministic STS component and (1, 1) 6∈ OI(C 0 ) = OI(C 00 ), C 00 is decomposable. From
this we have that D := feedback(C 00 ) is defined. Therefore, atomic(C) returns D and does not fail. It
remains to show that D has the desired properties. By the definition of feedback(C 00 ) and the fact that C 00
is a decomposable deterministic STS component, D is also a deterministic STS component. We also have:
D = feedback(C 00 ) ≡ fdbk(C 00 ) ≡ fdbk(C 0 ) = C
where feedback(C 00 ) ≡ fdbk(C 00 ) follows from Theorem 10 and fdbk(C 00 ) ≡ fdbk(C 0 ) follows from C 00 ≡ C 0
and the semantics of fdbk.
Finally, using Lemma 9 and OI(C 00 ) = OI(C 0 ), we have
OI(D) = OI(feedback(C 00 )) = OI(fdbk(C 00 )) = OI(fdbk(C 0 )) = OI(C)

Corollary 2. If a component C does not contain any fdbk operators or if determ(C) ∧ loop-free(C) is
true, then [[C]] is a GPT.
Note that condition determ(C) ∧ loop-free(C) is sufficient, but not necessary, for [[C]] to be a GPT.
For example, consider the following components:

Constfalse = stateless det x, true, false

And
= stateless det (x, y), true, (x ∧ y, x ∧ y)
C

= Constfalse ; fdbk(And)

Constfalse outputs the constant false. And is a version of logical and with two identical outputs (we need two
copies of the output, because one will be eliminated once we apply feedback). C is a composite component,
formed by first connecting the first output of And in feedback to its first input, and then connecting the
output of Constfalse to the second input of And (in reality, to the only remaining input of fdbk(And)).
Observe that C has algebraic loops, that is, loop-free(C) does not hold. Yet it can be shown that [[C]] is a
GPT (in particular, we can show that C ≡ Constfalse ).
Example.

The simplification algorithm applied to the component from Fig. 2 results in
atomic(Sum) = atomic(fdbk(Add ; UnitDelay ; Split)) = det(y, s, 0, s + y, s).

35

To see how the above is derived, let us first calculate atomic(Add ; UnitDelay ; Split):
atomic(Add ; UnitDelay ; Split)
=
serial(atomic(Add ; UnitDelay), Split)
=
serial(serial(Add, UnitDelay), Split)
= {Expanding Add and UnitDelay and choosing suitable variable names}
serial(serial(stateless det((x, y), true, x + y), det(z, s, 0, true, z, s)), Split)
=

{Computing inner serial}
serial(det((x, y), s, 0, true, x + y, s), Split)

=

{Expanding Split and choosing suitable variable names}
serial(det((x, y), s, 0, true, x + y, s), stateless det(z, true, (z, z)))

=

{Computing remaining serial}
det((x, y), s, 0, true, x + y, (s, s))

We calculate now atomic(fdbk(det((x, y), s, 0, true, x + y, (s, s)))):
atomic(fdbk(det((x, y), s, 0, true, x + y, (s, s))))
= {x is not free in s}
feedback(det((x, y), s, 0, true, x + y, (s, s)))
= {Computing feedback}
det(y, s, 0, true, s + y, s)

5.8

Checking Validity and Compatibility

Recall the example given in §5.3.7, of the serial composition of components C1 and C2 , resulting in a
component with input-output relation false, implying that [[C1 ; C2 ]] = Fail. When this occurs, we say that
C1 and C2 are incompatible. We would like to catch such incompatibilities. This amounts to first simplifying
the serial composition C1 ; C2 into an atomic component C, and then checking whether [[C]] = Fail.
In general, we say that a component C is valid if [[C]] 6= Fail. Given a component C, we can check
whether it is valid, as follows. First, we simplify C to obtain an atomic component C 0 = atomic(C). If C 0
is a QLTL component of the form qltl(x, y, ϕ) then C 0 is valid iff ϕ is satisfiable. The same is true if C 0 is
a stateless STS component of the form stateless(x, y, ϕ). If C 0 is a general STS component then we can
first transform it into a QLTL component and check satisfiability of the resulting QLTL formula.
Theorem 12. If C is an atomic component of the form qltl(x, y, ϕ) or stateless(x, y, ϕ), then [[C]] 6= Fail
iff ϕ is satisfiable.
As mentioned in the introduction, one of the goals of RCRS is to function as a behavioral type system
for reactive system modeling frameworks such as Simulink. In the RCRS setting, type checking consists
in checking properties such as compatibility of components, as in the example C1 ; C2 of §5.3.7. When
components are compatible, by computing new (stronger) input preconditions like in the example C3 ; C4
of §5.3.7, RCRS can be seen as enabling to perform behavioral type inference. Indeed, the new derived
condition G F x in the above example can be seen as an inferred type of the composite component C3 ; C4 .
We note that the decidability of the satisfiability question for ϕ depends on the logic used and the domains
of the variables in the formula. For instance, although ϕ can be a QLTL formula, if it restricts the set of

36

constants to true, has no functional symbols, and only equality as predicate symbol, then it is equivalent to
a QPTL formula,4 for which we can use available techniques [76].

5.9

Checking Input-Receptiveness and Computing Legal Inputs Symbolically

Given a component C, we often want to check whether it is input-receptive, i.e., whether legal([[C]]) = >,
or equivalently, [[C]](>) = >. More generally, we may want to compute the legal input values for C, which
is akin to type inference as discussed above. To do this, we will provide a symbolic method to compute
legal([[C]]) as a formula legal(C). Then, checking that C is input-receptive amounts to checking that the
formula legal(C) is valid, or equivalently, checking that ¬legal(C) is unsatisfiable. We assume that C is
atomic (otherwise, we first simplify C using the algorithm of §5.7).
Definition 22. Given an atomic component C, we define legal(C), a formula characterizing the legal inputs
of C. legal(C) is defined based on the type of C:

legal qltl(x, y, ϕ) = (∃y : ϕ)
(25)

0
legal sts(x, y, s, init, trs) = (∀s, y : init ⇒ (ϕ L ϕ ))
(26)

legal stateless(x, y, trs) = G (∃y : trs)
(27)

legal det(x, s, a, p, next, out) = (∀s, y : s = a ⇒ (# s = next ∧ y = out) L p)
(28)

(29)
legal stateless det(x, p, out) = G p
where ϕ = trs[s0 := # s] and ϕ0 = (∃s0 , y : trs).

The next theorem shows that legal correctly characterizes the semantic predicate legal:

Theorem 13. If C is an atomic component , then
legal([[C]]) = {σx | σx |= legal(C)}.
It follows from Theorem 13 that a component C is input-receptive iff the formula legal(C) is valid.

5.10

Checking Refinement Symbolically

We end this section by showing how to check whether a component refines another component. Again, we
will assume that the components in question are atomic (if not, they can be simplified using the atomic
procedure).
Theorem 14. Let C1 = sts(x, y, s, init, r1 ), C10 = sts(x, y, s, init0 , r10 ), C2 = stateless(x, y, r2 ), C20 =
stateless(x, y, r20 ), C3 = qltl(x, y, ϕ), and C30 = qltl(x, y, ϕ0 ). Then:
1. C1 is refined by C10 if the formula
(init0 ⇒ init) ∧ ((∃s0 , y : r1 ) ⇒ (∃s0 , y : r10 )) ∧ ((∃s0 , y : r1 ) ∧ r10 ⇒ r)
is valid.
2. C2 is refined by C20 if and only if the formula


(∃y : r2 ) ⇒ (∃y : r20 ) ∧ (∃y : r2 ) ∧ r20 ⇒ r2
is valid.
4

For example, the atomic QLTL formula # # x = # y can be translated into the LTL formula X X x ⇔ X y, and the
formula # # # x = true into X X X x.

37

3. C3 is refined by C30 if and only if the formula


(∃y : ϕ) ⇒ (∃y : ϕ0 ) ∧ ((∃y : ϕ) ∧ ϕ0 ) ⇒ ϕ
is valid.
As the above theorem shows, checking refinement amounts to checking validity (or equivalently, satisfiability of the negation) of first-order formulas formed by the various symbolic expressions in the component
specifications. The exact logic of these formulas depends on the logics used by the components. For example,
if C3 and C30 both use quantifier-free LTL for φ and φ0 , then in order to check refinement we need to check
satisfiability of a first-order QLTL formula.
Examples.

Consider again the QLTL component C = qltl((), t, oven), introduced in §3.3, where
oven =

(t = 20 ∧ ((t < # t ∧ t < 180) U thermostat))

thermostat = G (180 ≤ t ∧ t ≤ 220)
Let us introduce a refined version C 0 of C:
C0

=

sts((), t, (s, sw), init, trs) where

init =

s = 20 ∧ sw = on

trs

(t = s) ∧

=

(if sw = on then s < s0 < s + 5 else (if s > 10 then s − 5 < s0 < s else s0 = s)) ∧
(if sw = on ∧ s > 210 then sw0 = off else
(if sw = off ∧ s < 190 then sw0 = on else sw0 = sw))
C 0 is an STS component with no input variables, output variable t, and state variables s and sw, recording
the current temperature of the oven, and the on/off status of the switch, respectively. When sw is on, the
temperature increases nondeterministically by up to 5 units, otherwise the temperature decreases nondeterministically by up to 5 units. When the temperature exceeds 210, the switch is turned off; when the
temperature is below 190, the switch is turned on; otherwise sw remains unchanged. The output t is always
equal to the current state s. Initially the temperature is 20, and sw is on.
Using Theorem 14, and the properties of sts2qltl we have:
C  C0
⇐⇒
C  sts2qltl(C 0 )
⇐⇒
qltl((), t, oven)  qltl((), t, (∀s, sw, t : init ⇒ (ϕ L ϕ0 )) ∧ (∃s, sw : init ∧ G ϕ))
⇐⇒

where ϕ = trs[s0 , sw0 := # s, # sw] and ϕ0 = (∃s0 , sw0 , t : trs)

{Using Lemma 1, because ϕ0 ⇐⇒ true}

qltl((), t, oven)  qltl((), t, (∃s, sw : init ∧ G ϕ))
⇐⇒

{Using Theorem 14}


(∃t : oven) ⇒ (∃t, s, sw : init ∧ G ϕ) ∧ ((∃t : oven) ∧ (∃s, sw : init ∧ G ϕ)) ⇒ oven is valid

⇐⇒

{Because (∃t : oven) ⇐⇒ true and (∃t, s, sw : init ∧ G ϕ) ⇐⇒ true}

(∃s, sw : init ∧ G ϕ) ⇒ oven is valid

Thus, checking whether C 0 refines C amounts to checking whether the QLTL formula (∃s, sw : init∧G ϕ) ⇒
oven is valid. This indeed holds for this example and can be shown using logical reasoning.
38

The above example is relatively simple in the sense that in the end refinement reduces to checking
implication between the corresponding contracts. Indeed, this is always the case for input-receptive systems,
as in the example above. However, refinement is not equivalent to implication in the general case of noninput-receptive systems. For example, consider the components:
C1

= stateless(x, y, x ≥ 0 ∧ y ≥ x)

C2

= stateless(x, y, x ≤ y ≤ x + 10)

Using Theorem 14, we have:
C1  C2
⇐⇒

{Theorem 14}
((∃y : x ≥ 0 ∧ y ≥ x) ⇒ (∃y : x ≤ y ≤ x + 10)) ∧
((∃y : x ≥ 0 ∧ y ≥ x) ∧ x ≤ y ≤ x + 10 ⇒ x ≥ 0 ∧ y ≥ x) is valid

⇐⇒

{Arithmetic and logical reasoning}
true

Note that the second and third parts of Theorem 14 provide necessary and sufficient conditions, while
the first part only provides a sufficient, but generally not necessary condition. Indeed, the condition is
generally not necessary in the case of STS components with state, as state space computation is ignored by
the condition. This can be remedied by transforming STS components into equivalent QLTL components
and then applying the second part of the theorem. An alternative which may be more tractable, particularly
in the case of finite-state systems, is to use techniques akin to strategy synthesis in games, such as those
proposed in [79] for finite-state relational interfaces.
Another limitation of the first part of Theorem 14 is that it requires the two STS components to have
the same state space, i.e., the same state variable s. This restriction can be lifted using the well-known idea
of data refinement [44, 8].
Theorem 15. Let C1 = sts(x, y, s, init, r), C2 = sts(x, y, t, init0 , r0 ) be two STS components, and D a
(data refinement) expression on variables s and t. Let p = (∃s0 , y : r) and p0 = (∃t0 , y : r0 ). If the formulas
(∀t : init0 ⇒ (∃s : D ∧ init))
(∀t, x, s : D ∧ p ⇒ p0 )
(∀t, x, s, t0 , y : D ∧ p ∧ r0 ⇒ (∃s0 : D[t, s := t0 , s0 ] ∧ r))
are valid, then C1 is refined by C2 .

6

Toolset and Case Studies

The RCRS framework comes with a toolset, illustrated in Fig. 8. The toolset is publicly available under
the MIT license and can be downloaded from http://rcrs.cs.aalto.fi. The toolset is described in tool
papers [32, 33] ([32] contains additional material over [33], specifically, a six-page appendix describing a
demo of the RCRS toolset). In summary, the toolset consists of:
• A full implementation of the RCRS theory in Isabelle [61]. The implementation consists of 22 theory
files and a total of 27588 lines of Isabelle code. A detailed description of the implementation can be
found in the file document.pdf available in the public distribution of RCRS.
• A formal Analyzer, which is a set of procedures implemented on top of Isabelle and the functional
programming language SML. The Analyzer performs compatibility checking, automatic contract simplification, and other functions.
39

Options
(translation strategy, etc.)
Fuel Control System Model

RCRS theory and component library
(Isabelle theory ﬁles)

This model uses only the ODEs to implement the dynamics.

theta [0 90]
1
throttle input (deg)
[0, 81.2]

1
.1s+1

1
A/F

Throttle del ay1
1
s

f(u)

8.8

ODE1

Base opening angle

~=

1
s

1
s

f(u)

pe

ODE4 Closed

double

2

~=

Fuel Cmd Open Pwr

Analyzer

f(u)

0.0

f(u)

airbyfuel_ref

14.7

lambda

f(u)
ODE3

incompatiblity detection

12.5

p

f(u)
ODE2

ODE4 Open

~=

Fuel Cmd Open

1
s

~=

i
f(u)
f(u)

Fuel Cmd Closed

InputPoly

2
engine speed (rpm)
[900,1100]

pi/30

AND

(rpm) to (rad/s)

internal variable elimination

Power Mode Guard
boolean
Starup Mode

1: Failure
0: Normal

In

Out

Startup Mode Latch

boolean
FaultInjection

In

Out

Sensor Failure Detection Latch

OR

3
controller_mode
NOT

Powertrain Control Benchmark Model
Toyota Technial Center
2014
This is a model of a hybrid automaton with polynomial dynamics, and an implementation of the 3rd model that appears in
"Powertrain Control Veriﬁcation Benchmark", 2014 Hybrid Systems: Computation and Control,
X. Jin, J. V. Deshmukh, J.Kapinski, K. Ueda, and K. Butts

Simulink
diagram

Translator
RCRS model
of the diagram

(built on top of
Isabelle
theorem prover)

auto generated top-level contract
reﬁnement checking
...

Figure 8: The RCRS toolset.
• A formalization of Simulink characterizing basic Simulink blocks as RCRS components and implementing those as a library of RCRS/Isabelle. At the time of writing this paper, 48 of Simulink’s blocks can
be handled.
• A Translator : a Python program translating Simulink hierarchical block diagrams into RCRS code.
We implemented in Isabelle a shallow embedding [14] of the language introduced in §3. The advantage of
a shallow embedding is that all datatypes of Isabelle are available for specification of components, and we
can use the existing Isabelle mechanism for renaming bound variables in compositions. The disadvantage
of this shallow embedding is that we cannot express Algorithm 7 within Isabelle (hence the “manual” proof
that we provide for Theorem 11). A deep embedding, in which the syntax of components is defined as a
datatype of Isabelle, is possible, and is left as an open future work direction.
We implemented Algorithm 7 in SML, the meta-language of Isabelle. The SML program takes as input
a component C and returns not only a simplified atomic component atomic(C), but also a proved Isabelle
theorem of the fact C ≡ atomic(C). The simplification program, as well as a number of other procedures
to perform compatibility checking, validity checking, etc., form what we call the Analyzer in Fig. 8.
The Translator takes as input a Simulink model and produces an RCRS/Isabelle theory file containing: (1)
the definition of all atomic and composite components representing the Simulink diagram; and (2) embedded
bottom-up simplification procedures and the corresponding correctness theorems. By running this theory
file in Isabelle, we obtain an atomic component corresponding to the top-level Simulink model, equivalent to
the original composite component. As a special case, if the Simulink diagram contains inconsistencies (e.g.,
division by zero), these are detected by obtaining Fail as the top-level atomic component. The error can be
localized by finding earlier points in the Simulink hierarchy (subsystems) which already resulted in Fail.
As mentioned earlier, how to obtain a composite component from a graphical block diagram is an interesting problem. This problem is studied in depth in [31], where several translation strategies are proposed.
These various strategies all yield semantically equivalent components, but with different trade-offs in terms
of size, readability, effectiveness of the simplification procedures, and so on. The Translator implements all
these translation strategies, allowing the user to explore these trade-offs. Further details on the translation
problem are provided in [31, 65]. A proof that the translation strategies yield semantically equivalent components is provided in [64]. This proof, which has been formalized in Isabelle, is a non-trivial result: the
entire formalization of the translation algorithms and the proof is 13579 lines of Isabelle code.
We have used the RCRS toolset on several case studies, including a real-life benchmark provided by
the Toyota motor company. The benchmark involves a Fuel Control System (FCS) described in [45, 46].
FCS aims at controlling the air mass and injected fuel in a car engine such that their ratio is always
optimal. This problem has important implications on lowering pollution and costs by improving the engine
performance. Toyota has made several versions of FCS publicly available as Simulink models at https:
//cps-vo.org/group/ARCH/benchmarks.
We have used the RCRS toolset to process two of the three Simulink models in the FCS benchmark suite
(the third model contains blocks that are currently not implemented in the RCRS component library). A
40

typical model in this set has a 3-layer hierarchy with a total of 104 Simulink block instances (97 basic blocks
and 7 subsystems), and 101 connections out of which 8 are feedbacks. Each basic Simulink block is modeled in
our framework by an atomic STS component (possibly stateless). These atomic STS components are created
once, and form part of the RCRS implementation, which is reused for different Simulink models. The
particular FCS diagram is translated into RCRS using the Translator, and simplified within Isabelle using
our SML simplification procedure. After simplification, we obtain an atomic deterministic STS component
with no inputs, 7 outputs, and 14 state variables. Its contract (which is 8337 characters long) includes a
condition on the state variables, in particular, that a certain state variable must always be non-negative (as
its value is fed into a square-root block). This condition makes it not immediately obvious that the whole
system is valid (i.e., not Fail). However, we can show after applying the transformation sts2qltl that the
resulting formula is satisfiable, which implies that the original model is consistent (i.e., no connections result
in incompatibilities, there are no divisions by zero, etc.). This illustrates the use of RCRS as a powerful
static analysis tool. More details on the FCS case study are provided in [31, 65, 32].

7

Related Work

Several formal compositional frameworks exist in the literature. Most closely related to RCRS are the
frameworks of FOCUS [15], input-output automata [54], reactive modules [6], interface automata [22], and
Dill’s trace theory [29]. RCRS shares with these frameworks many key compositionality principles, such as
the notion of refinement. At the same time, RCRS differs and complements these frameworks in important
ways. Specifically, FOCUS, IO-automata, and reactive modules, are limited to input-receptive systems,
while RCRS is explicitly designed to handle non-input-receptive specifications. The benefits of non-inputreceptiveness are discussed extensively in [79] and will not be repeated here. Interface automata are a
low-level formalism whereas RCRS specifications and reasoning are symbolic. For instance, in RCRS one
can naturally express systems with infinite state-spaces, input-spaces, or output-spaces. (Such systems can
even be handled automatically, provided the corresponding logic they are expressed in is decidable.) Both
interface automata and Dill’s trace theory use a single form of asynchronous parallel composition, whereas
RCRS has three primitive composition operators (serial, parallel, feedback) with synchronous semantics.
Our work adapts and extends to the reactive system setting many of the ideas developed previously in a
long line of research on correctness and compositionality for sequential programs. This line of research goes
back to the works of Floyd, Hoare, Dijkstra, and Wirth, on formal program semantics, weakest preconditions,
program development by stepwise refinement, and so on [34, 43, 27, 81]. It also goes back to game-theoretic
semantics of sequential programs as developed in the original refinement calculus [10], as well as to contractbased design [57]. Many of the concepts used in our work are in spirit similar to those used in the above
works. For instance, an input-output formula φ used in an atomic component in our language can be seen
as a contract between the environment of the component and the component itself: the environment must
satisfy the contract by providing to the component legal inputs, and the component must in turn provide
legal outputs (for those inputs). On the other hand, several of the concepts used here come from the world
of reactive systems and as such do not have a direct correspondence in the world of sequential programs.
For instance, this is the case with feedback composition.
RCRS extends refinement calculus from predicate to property transformers. Extensions of refinement
calculus to infinite behaviors have also been proposed in the frameworks of action systems [11], fair action
systems [12], and Event B [3]. These frameworks use predicate (not property) transformers as semantic
foundation; they can handle certain property patterns (e.g., fairness) by providing proof rules for these
properties, but they do not treat livenes and LTL properties in general [12, 82, 42]. The Temporal Logic of
Actions [49] can be used to specify liveness properties, but does not distinguish between inputs and outputs,
and as such cannot express non-input-receptive components.
Our specifications can be seen as “rich”, behavioral types [50, 22]. Indeed, our work is closely related to
programming languages and type theory, specifically, refinement types [35], behavioral types [60, 51, 26], and
liquid types [69].
Behavioral type frameworks have also been proposed in reactive system settings. In the SimCheck
41

framework [70], Simulink blocks are annotated with constraints on input and output variables, much like
stateless components in RCRS. RCRS is more general as it also allows to specify stateful components. RCRS
is also a more complete compositional framework, with composition operators and refinement, which are not
considered in [70]. Other behavioral type theories for reactive systems have been proposed in [23, 18, 30].
Compared to RCRS, these works are less general. In particular, [23, 30] are limited to specifications which
separate the assumptions on the inputs from the guarantees on the outputs, and as such cannot capture
input-output relations. [18] considers a synchronous model which allows to specify legal values of inputs and
outputs at the next step, given the current state. This model does not allow to capture relations between
inputs and outputs within the same step, which RCRS allows.
Our work is related to formal verification frameworks for hybrid systems [5]. Broadly speaking, these
can be classified into frameworks following a model-checking approach, which typically use automata-based
specification languages and state-space exploration techniques, and those following a theorem-proving approach, which typically use logic-based specifications. More closely related to RCRS are the latter, among
which, CircusTime [17], KeYmaera [37], and the PVS-based approach in [2]. CircusTime can handle a larger
class of Simulink diagrams than the current implementation of RCRS. In particular, CircusTime can handle
multi-rate diagrams, where different parts of the model work at different rates (periods). On the other hand,
CircusTime is based on predicate (not property) transformers, and as such cannot handle liveness properties. KeYmaera is a theorem prover based on differential dynamic logic [62], which is itself based on dynamic
logic [39]. The focus of both KeYmaera and the work in [2] is verification, and not compositionality. For
instance, these works do not distinguish between inputs and outputs and do not investigate considerations
such as input-receptiveness. The work of [68] distinguishes inputs and outputs, but provides a system model
where the output relation is separated from the transition relation, and where the output relation is assumed
to be total, meaning that there exists an output for every input and current state combination. This does
not allow to specify non-input-receptive stateless components, such as for example the Div component from
§3.
Our component algebra is similar to the algebra of flownomials [77] and to the relational model for nondeterministic dataflow [41]. In [20], graphs and graph operations which can be viewed as block diagrams
are represented by algebraic expressions and operations, and a complete equational axiomatization of the
equivalence of the graph expressions is given. This is then applied to flow-charts as investigated in [72]. The
translation of block diagrams in general and Simulink in particular has been treated in a large number of
papers, with various goals, including verification and code generation (e.g., see [80, 56, 19, 52, 73, 13, 83, 84,
85, 58]). Although we share several of the ideas of the above works, our main goal here is not to formalize
the language of block diagrams, neither their translation to other formalisms, but to provide a complete
compositional framework for reasoning about reactive systems.
RCRS is naturally related to compositional verification frameworks, such as [38, 1, 55, 74, 40, 24, 25].
In particular, compositional verification frameworks often make use of a refinement relation such as trace
inclusion or simulation [74, 40]. However, the focus of these frameworks is different than that of RCRS.
In compositional verification, the focus is to “break down” a large (and usually computationally expensive)
verification task into smaller (and hopefully easier to calculate) subtasks. For this purpose, compositional
verification frameworks employ several kinds of decomposition rules. An example of such a rule is the socalled precongruence rule (i.e., preservation of refinement by composition): if P1 refines Q1 , and P2 refines
Q2 , then the composition P1 kP2 refines Q1 kQ2 . This, together with preservation of properties by refinement,
allows us to conclude that P1 kP2 satisfies some property φ, provided we can prove that Q1 kQ2 satisfies φ.
The latter might be a simpler verification task, if Q1 and Q2 are smaller than P1 and P2 . The essence of
compositional verification is in finding such abstract versions Q1 and Q2 of the concrete processes in question,
P1 and P2 , and employing decomposition rules like the one above in the hope of making verification simpler.
RCRS can also be used for compositional verification: indeed, RCRS provides both the precongruence rule,
and preservation of properties by refinement. Note that, in traditional settings, precongruence is not always
powerful enough, and for this reason most compositional verification frameworks employ more complex
decomposition rules (e.g., see [59]). In settings which allow non-input-receptive components, such as ours,
there are indications that the precongruence rule is sufficient for compositional verification purposes [75],

42

although more work is required to establish this in the specific context of RCRS. Such work is beyond the
scope of the current paper. We also note that, beyond compositional verification with precongruence, RCRS
provides a behavioral type theory which allows to state system properties such as compatibility, which is
typically not available in compositional verification frameworks.
Refinement can be seen as the inverse of abstraction, and as such our framework is related to general
frameworks such as abstract interpretation [21]. Several abstractions have been proposed in reactive system
settings, including relational abstractions for hybrid systems, which are related to Simulink [71]. The focus
of these works is verification, and abstraction is used as a mechanism to remove details from the model
that make verification harder. In RCRS, the simplification procedure that we employ can be seen as an
abstraction process, as it eliminates internal variable information. However, RCRS simplification is an exact
abstraction, in the sense that it does not lose any information: the final system is equivalent to the original
one, and not an over- or under-approximation, as is usually the case with typical abstractions for verification
purposes.

8

Conclusion

We presented RCRS, a compositional framework for modeling and reasoning about reactive systems. This
paper focuses on the theory and methodology of RCRS, its formal semantics, and techniques for symbolic
and computer-aided reasoning.
RCRS is an ongoing project, and a number of problems remain open. Future work directions include:
• An extension of the framework to systems with algebraic loops, which necessitates handling instantaneous feedback. Here, the preliminary ideas of [67] can be helpful in defining the semantics of instantaneous feedback. However, [67] does not provide solutions on how to obtain symbolic closed-form
expression for the feedback of general components.
• Extension of the results of §5.5 to general components, possibly non-deterministic or non-decomposable.
• An extension of the framework to acausal systems, i.e., systems without a clear distinction of inputs
and outputs [36].
• The development of better symbolic reasoning techniques, such as simplification of logical formulas,
decision procedures, etc.

References
[1] M. Abadi and L. Lamport. Conjoining specifications. ACM Trans. Program. Lang. Syst., 17(3):507–535,
1995.
[2] E. Ábrahám-Mumm, M. Steffen, and U. Hannemann. Verification of hybrid systems: Formalization
and proof rules in PVS. In 7th Intl. Conf. Engineering of Complex Computer Systems (ICECCS 2001),
pages 48–57, 2001.
[3] J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, New
York, NY, USA, 1st edition, 2010.
[4] B. Alpern and F. B. Schneider. Defining liveness. Information Processing Letters, 21(4):181 – 185, 1985.
[5] R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and
S. Yovine. The algorithmic analysis of hybrid systems. Theoretical Computer Science, 138:3–34, 1995.
[6] R. Alur and T. Henzinger. Reactive modules. Formal Methods in System Design, 15:7–48, 1999.

43

[7] R. Alur, T. Henzinger, O. Kupferman, and M. Vardi. Alternating refinement relations. In CONCUR’98,
volume 1466 of LNCS. Springer, 1998.
[8] R. J. Back. Correctness preserving program refinements: proof theory and applications, volume 131 of
Mathematical Centre Tracts. Mathematisch Centrum, Amsterdam, 1980.
[9] R.-J. Back and M. Butler. Exploring summation and product operators in the refinement calculus, pages
128–158. Springer Berlin Heidelberg, Berlin, Heidelberg, 1995.
[10] R.-J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer, 1998.
[11] R.-J. Back and J. Wright. Trace refinement of action systems. In B. Jonsson and J. Parrow, editors,
CONCUR ’94: Concurrency Theory, volume 836 of Lecture Notes in Computer Science, pages 367–384.
Springer Berlin Heidelberg, 1994.
[12] R.-J. Back and Q. Xu. Refinement of fair action systems. Acta Informatica, 35(2):131–165, 1998.
[13] P. Boström. Contract-Based Verification of Simulink Models. In S. Qin and Z. Qiu, editors, Formal
Methods and Software Engineering, volume 6991 of Lecture Notes in Computer Science, pages 291–306.
Springer Berlin Heidelberg, 2011.
[14] R. J. Boulton, A. Gordon, M. J. C. Gordon, J. Harrison, J. Herbert, and J. V. Tassel. Experience with
embedding hardware description languages in HOL. In IFIP TC10/WG 10.2 Intl. Conf. on Theorem
Provers in Circuit Design, pages 129–156. North-Holland Publishing Co., 1992.
[15] M. Broy and K. Stølen. Specification and development of interactive systems: focus on streams, interfaces, and refinement. Springer, 2001.
[16] R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and
S. Tonetta. The nuxmv symbolic model checker. In A. Biere and R. Bloem, editors, Computer Aided
Verification: 26th International Conference, CAV 2014,, pages 334–342, Cham, 2014. Springer.
[17] A. L. C. Cavalcanti, A. Mota, and J. C. P. Woodcock. Simulink timed models for program verification.
In Z. Liu, J. C. P. Woodcock, and H. Zhu, editors, Theories of Programming and Formal Methods Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, volume 8051 of Lecture Notes in
Computer Science, pages 82–99. Springer, 2013.
[18] A. Chakrabarti, L. de Alfaro, T. Henzinger, and F. Mang. Synchronous and bidirectional component
interfaces. In CAV, LNCS 2404, pages 414–427. Springer, 2002.
[19] C. Chen, J. S. Dong, and J. Sun. A formal framework for modeling and validating Simulink diagrams.
Formal Aspects of Computing, 21(5):451–483, 2009.
[20] B. Courcelle. A representation of graphs by algebraic expressions and its use for graph rewriting
systems. In H. Ehrig, M. Nagl, G. Rozenberg, and A. Rosenfeld, editors, Graph-Grammars and Their
Application to Computer Science, 3rd International Workshop, Warrenton, Virginia, USA, December
2-6, 1986, volume 291 of Lecture Notes in Computer Science, pages 112–132. Springer, 1986.
[21] P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs
by construction or approximation of fixpoints. In 4th ACM Symp. POPL, 1977.
[22] L. de Alfaro and T. Henzinger. Interface automata. In Foundations of Software Engineering (FSE).
ACM Press, 2001.
[23] L. de Alfaro and T. Henzinger. Interface theories for component-based design. In EMSOFT’01. Springer,
LNCS 2211, 2001.

44

[24] W. de Roever, H. Langmaack, and A. E. Pnueli. Compositionality: The Significant Difference. LNCS.
Springer, 1998.
[25] W.-P. de Roever, F. de Boer, U. Hanneman, J. Hooman, Y. Lakhnech, M. Poel, and J. Zwiers. Concurrency Verification: Introduction to Compositional and Non-compositional Methods. Cambridge University Press, 2012.
[26] K. Dhara and G. Leavens. Forcing behavioral subtyping through specification inheritance. In ICSE’96:
18th Intl. Conf. on Software Engineering, pages 258–267. IEEE Computer Society, 1996.
[27] E. Dijkstra. Notes on structured programming. In O. Dahl, E. Dijkstra, and C. Hoare, editors, Structured
programming, pages 1–82. Academic Press, London, UK, 1972.
[28] E. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Comm. ACM,
18(8):453–457, 1975.
[29] D. Dill. Trace theory for automatic hierarchical verification of speed-independent circuits. MIT Press,
Cambridge, MA, USA, 1987.
[30] L. Doyen, T. Henzinger, B. Jobstmann, and T. Petrov. Interface theories with component reuse. In 8th
ACM & IEEE International conference on Embedded software, EMSOFT, pages 79–88, 2008.
[31] I. Dragomir, V. Preoteasa, and S. Tripakis. Compositional Semantics and Analysis of Hierarchical Block
Diagrams. In SPIN, pages 38–56. Springer, 2016.
[32] I. Dragomir, V. Preoteasa, and S. Tripakis. The Refinement Calculus of Reactive Systems Toolset.
CoRR, abs/1710.08195, 2017.
[33] I. Dragomir, V. Preoteasa, and S. Tripakis. The Refinement Calculus of Reactive Systems Toolset. In
TACAS, 2018.
[34] R. Floyd. Assigning meanings to programs. In In. Proc. Symp. on Appl. Math. 19, pages 19–32.
American Mathematical Society, 1967.
[35] T. Freeman and F. Pfenning. Refinement Types for ML. SIGPLAN Not., 26(6):268–277, May 1991.
[36] P. Fritzson. Principles of Object-Oriented Modeling and Simulation with Modelica 3.3: A Cyber-Physical
Approach. Wiley, 2 edition, 2014.
[37] N. Fulton, S. Mitsch, J.-D. Quesel, M. Völp, and A. Platzer. KeYmaera X: An axiomatic tactical
theorem prover for hybrid systems. In A. P. Felty and A. Middeldorp, editors, CADE, volume 9195 of
LNCS, pages 527–538. Springer, 2015.
[38] O. Grumberg and D. Long. Model checking and modular verification. ACM Trans. Program. Lang.
Syst., 16(3):843–871, 1994.
[39] D. Harel, J. Tiuryn, and D. Kozen. Dynamic Logic. MIT Press, 2000.
[40] T. Henzinger, S. Qadeer, and S. Rajamani. You assume, we guarantee: Methodology and case studies.
In CAV’98, volume 1427 of LNCS. Springer-Verlag, 1998.
[41] T. T. Hildebrandt, P. Panangaden, and G. Winskel. A relational model of non-deterministic dataflow.
Mathematical Structures in Computer Science, 14(5):613–649, 10 2004.
[42] T. S. Hoang and J.-R. Abrial. Reasoning About Liveness Properties in Event-B. In Proceedings of the
13th International Conference on Formal Methods and Software Engineering, ICFEM’11, pages 456–471,
Berlin, Heidelberg, 2011. Springer-Verlag.

45

[43] C. A. R. Hoare. An axiomatic basis for computer programming. Comm. ACM, 12(10):576–580, 1969.
[44] C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1(4), Dec. 1972.
[45] X. Jin, J. Deshmukh, J. Kapinski, K. Ueda, and K. Butts. Benchmarks for model transformations
and conformance checking. In 1st Intl. Workshop on Applied Verification for Continuous and Hybrid
Systems (ARCH), 2014.
[46] X. Jin, J. V. Deshmukh, J. Kapinski, K. Ueda, and K. Butts. Powertrain Control Verification Benchmark. In Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC’14, pages 253–262. ACM, 2014.
[47] Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification of simulation and refinement. In J. W.
de Bakker, W. P. de Roever, and G. Rozenberg, editors, A Decade of Concurrency Reflections and
Perspectives: REX School/Symposium, pages 273–346. Springer, 1994.
[48] Y. Kesten and A. Pnueli. Complete Proof System for QPTL. Journal of Logic and Computation,
12(5):701, 2002.
[49] L. Lamport. The temporal logic of actions. ACM Trans. Program. Lang. Syst., 16(3):872–923, May
1994.
[50] E. Lee and Y. Xiong. System-level types for component-based design. In EMSOFT’01: 1st Intl.
Workshop on Embedded Software, pages 237–253. Springer, 2001.
[51] B. Liskov and J. Wing. A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst., 16(6):1811–
1841, 1994.
[52] R. Lublinerman, C. Szegedy, and S. Tripakis. Modular code generation from synchronous block diagrams
– modularity vs. code size. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages (POPL’09), pages 78–89. ACM, Jan. 2009.
[53] R. Lublinerman and S. Tripakis. Modularity vs. reusability: Code generation from synchronous block
diagrams. In Design, Automation, and Test in Europe (DATE’08), pages 1504–1509. ACM, Mar. 2008.
[54] N. Lynch and M. Tuttle. An introduction to input/output automata. CWI Quarterly, 2:219–246, 1989.
[55] K. McMillan. A compositional rule for hardware design refinement. In Computer Aided Verification
(CAV’97), volume 1254 of LNCS. Springer-Verlag, 1997.
[56] B. Meenakshi, A. Bhatnagar, and S. Roy. Tool for Translating Simulink Models into Input Language of
a Model Checker. In Formal Methods and Software Engineering, volume 4260 of LNCS, pages 606–620.
Springer, 2006.
[57] B. Meyer. Applying “Design by Contract”. Computer, 25(10):40–51, 1992.
[58] S. Minopoli and G. Frehse. SL2SX Translator: From Simulink to SpaceEx Verification Tool. In 19th
ACM International Conference on Hybrid Systems: Computation and Control (HSCC), 2016.
[59] K. S. Namjoshi and R. J. Trefler. On the completeness of compositional reasoning methods. ACM
Trans. Comput. Logic, 11(3), 2010.
[60] O. Nierstrasz. Regular types for active objects. SIGPLAN Not., 28(10):1–15, 1993.
[61] T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic.
LNCS 2283. Springer, 2002.
[62] A. Platzer. Differential dynamic logic for hybrid systems. J. Autom. Reas., 41(2):143–189, 2008.
46

[63] A. Pnueli. The Temporal Logic of Programs. In 18th Annual Symposium on Foundations of Computer
Science, Providence, Rhode Island, USA, 31 October - 1 November 1977, pages 46–57. IEEE Computer
Society, 1977.
[64] V. Preoteasa, I. Dragomir, and S. Tripakis. A nondeterministic and abstract algorithm for translating
hierarchical block diagrams. CoRR, abs/1611.01337, 2016.
[65] V. Preoteasa, I. Dragomir, and S. Tripakis. Type Inference of Simulink Hierarchical Block Diagrams in
Isabelle. In 37th IFIP WG 6.1 International Conference on Formal Techniques for Distributed Objects,
Components, and Systems (FORTE), 2017.
[66] V. Preoteasa and S. Tripakis. Refinement calculus of reactive systems. In Embedded Software (EMSOFT), 2014 International Conference on, pages 1–10, Oct 2014.
[67] V. Preoteasa and S. Tripakis. Towards Compositional Feedback in Non-Deterministic and Non-InputReceptive Systems. In 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS),
2016.
[68] G. Reissig, A. Weber, and M. Rungger. Feedback refinement relations for the synthesis of symbolic
controllers. IEEE Trans. Automat. Contr., 62(4):1781–1796, 2017.
[69] P. M. Rondon, M. Kawaguci, and R. Jhala. Liquid types. In 29th ACM SIGPLAN Conference on
Programming Language Design and Implementation, PLDI ’08, pages 159–169, New York, NY, USA,
2008. ACM.
[70] P. Roy and N. Shankar. SimCheck: An expressive type system for Simulink. In C. Muñoz, editor,
2nd NASA Formal Methods Symposium (NFM 2010), NASA/CP-2010-216215, pages 149–160, Langley
Research Center, Hampton VA 23681-2199, USA, Apr. 2010. NASA.
[71] S. Sankaranarayanan and A. Tiwari. Relational abstractions for continuous and hybrid systems. In
Computer Aided Verification: 23rd International Conference, CAV 2011, pages 686–702. Springer, 2011.
[72] H. Schmeck. Algebraic characterization of reducible flowcharts. Journal of Computer and System
Sciences, 27(2):165 – 199, 1983.
[73] V. Sfyrla, G. Tsiligiannis, I. Safaka, M. Bozga, and J. Sifakis. Compositional translation of Simulink
models into synchronous BIP. In Industrial Embedded Systems (SIES), 2010 International Symposium
on, pages 217–220, July 2010.
[74] N. Shankar. Lazy compositional verification. In COMPOS’97: Revised Lectures from the International Symposium on Compositionality: The Significant Difference, pages 541–564, London, UK, 1998.
Springer-Verlag.
[75] A. Siirtola, S. Tripakis, and K. Heljanko. When do we not need complex assume-guarantee rules? ACM
Trans. Embed. Comput. Syst., 16(2):48:1–48:25, Jan. 2017.
[76] A. P. Sistla, M. Y. Vardi, and P. Wolper. The Complementation Problem for Büchi Automata with
Applications to Temporal Logic. Theoretical Computer Science, 49:217–237, 1987.
[77] G. Stefănescu. Network Algebra. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2000.
[78] S. Tripakis, B. Lickly, T. Henzinger, and E. Lee. On Relational Interfaces. In Proceedings of the 9th ACM
& IEEE International Conference on Embedded Software (EMSOFT’09), pages 67–76. ACM, 2009.
[79] S. Tripakis, B. Lickly, T. A. Henzinger, and E. A. Lee. A Theory of Synchronous Relational Interfaces.
ACM Trans. Program. Lang. Syst., 33(4):14:1–14:41, July 2011.

47

[80] S. Tripakis, C. Sofronis, P. Caspi, and A. Curic. Translating Discrete-time Simulink to Lustre. ACM
Trans. Embed. Comput. Syst., 4(4):779–818, Nov. 2005.
[81] N. Wirth. Program development by stepwise refinement. Comm. ACM, 14(4):221–227, 1971.
[82] D. Yadav and M. Butler. Verification of liveness properties in distributed systems. In Contemporary Computing, volume 40 of Communications in Computer and Information Science, pages 625–636.
Springer Berlin Heidelberg, 2009.
[83] C. Yang and V. Vyatkin. Transformation of Simulink models to IEC 61499 Function Blocks for verification of distributed control systems. Control Engineering Practice, 20(12):1259–1269, 2012.
[84] C. Zhou and R. Kumar. Semantic Translation of Simulink Diagrams to Input/Output Extended Finite
Automata. Discrete Event Dynamic Systems, 22(2):223–247, 2012.
[85] L. Zou, N. Zhany, S. Wang, M. Franzle, and S. Qin. Verifying Simulink diagrams via a Hybrid Hoare
Logic Prover. In Embedded Software (EMSOFT), Sept 2013.

48

