# Rule-Based Form for Stream Constraints

Kasper Dokter, Farhad Arbab

► To cite this version:

Kasper Dokter, Farhad Arbab. Rule-Based Form for Stream Constraints. 20th International Conference on Coordination Languages and Models (COORDINATION), Jun 2018, Madrid, Spain. pp.142-161, 10.1007/978-3-319-92408-3_6. hal-01821489

HAL Id: hal-01821489

https://inria.hal.science/hal-01821489

Submitted on 22 Jun 2018

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Rule-Based Form for Stream Constraints

Kasper Dokter and Farhad Arbab

Centrum Wiskunde & Informatica, Amsterdam, Netherlands

**Abstract.** Constraint automata specify protocols as labeled transition systems that preserve synchronization under composition. They have been used as a basis for tools, such as compilers and model checkers. Unfortunately, composition of transition systems suffers from state space and transition space explosions, which limits scalability of the tools based on constraint automata. In this work, we propose stream constraints as an alternative to constraint automata that avoids state space explosions. We introduce a rule-based form for stream constraints that can avoid transition space explosions. We provide sufficient conditions under which our approach avoids transition space explosions.

# 1 Introduction

Over a decade ago, Baier et al. introduced constraint automata for the specification of interaction protocols [6]. Constraint automata feature a powerful composition operator that preserves synchrony: composite constructions not only yield intuitively meaningful asynchronous protocols but also synchronous protocols. Constraint automata have been used as basis for tools, like compilers and model checkers. Jongmans developed Lykos: a compiler that translates constraint automata into reasonably efficient executable Java code [13]. Baier, Blechmann, Klein, and Klüppelholz developed Vereofy, a model checker for constraint automata [4,19]. Unfortunately, like every automaton model, composition of constraint automata suffers from state space and transition space explosions. These explosions limit the scalability of the tools based on constraint automata.

To improve scalability, Clarke et al. developed a compiler that translates a constraint automaton to a first-order formula [9]. The transitions of the constraint automaton correspond to the solutions of this formula. At run time, a generic constraint solver finds these solutions and simulates the automaton. Since composition and abstraction for constraint automata respectively correspond to conjunction and existential quantification, the first-order specification does not suffer from state space or transition space explosion. However, the approach proposed by Clarke et al. only delays the complexity until run time: calling a generic constraint solver at run time imposes a significant overhead.

Jongmans realized that the overhead of this constraint solver is not always necessary. He developed a commandification algorithm that accepts constraints without disjunctions (i.e., conjunctions of literals) and translates them into a small imperative program [14]. The resulting program is a light-weight, tailor-made constraint solver with minimal run time overhead. Since commandification
accepts only constraints without disjunction, Jongmans applied this technique to data constraints on individual transitions in a constraint automaton. Relying on constraint automata, his approach still suffers from scalability issues [17].

We aim to prevent state space and transition space explosions by combining the ideas of Clarke et al. and Jongmans. To this end, we present the language of *stream constraints*: a generalization of constraint automata based on temporal logic. A stream constraint is an expression that relates streams of observed data at different locations (Section 2). We identify a subclass of stream constraints, called *regular (stream) constraints*, which is closed under composition and abstraction (Section 3). Regular constraints can be viewed as a constraint automata, and conjunction of reflexive regular constraints is similar to composition of constraint automata (Section 4).

A straightforward application of the commandification algorithm of Jongmans to regular stream constraints entails transforming a stream constraint into disjunctive normal form and applying the algorithm to each clause separately. However, the number of clauses in the disjunctive normal form may grow exponentially in the size of the composition. To prevent such exponential blowups of the size of the formula, we recognize and exploit symmetries in the disjunctive normal form. Each clause in the disjunctive normal form can be constructed from a set of basic stream constraints, which we call *rules*. This idea allows us to represent a single large constraint as certain combination of a set of smaller constraints, called the *rule-based form* (Section 5). We express the composition of stream constraints in terms of the rule-based normal form (Section 6), and show that, for *simple* sets of rules, the number of rules to describe the composition is only linear in the size of the composition (Section 7). The class of stream constraints defined by a simple set of rules contains constraints for which the size of the disjunctive normal form explodes, which shows that our approach improves upon existing approaches by Clarke et al. and Jongmans. We express abstraction on stream constraints in terms of the rule-based normal form and provide a sufficient condition under which the number of rules remains constant (Section 8). Finally, we conclude and point out future work (Section 10).

*Related work* Representation of stream constraints in rule-based form is part of a larger line of research on symbolic approaches, such a symbolic model checking [8,5,20] and symbolic execution [10]. These approaches not only use logic (cf., SAT solving techniques [18,12] for verification), but also other implicit representations, like binary decision diagrams [7] and Petri nets [21]. Petri nets offer a small representation of protocols with an exponentially large state space. While our focus is more on compilation, Petri nets have been studied in the context of verification. As inspiration for future work, it is interesting to study the similarities between Petri nets and stream constraints.

Since regular stream constraints correspond to constraint automata, we can view regular stream constraints as a restricted temporal logic for which distributed synthesis is easy. In general, distributed (finite state) synthesis of protocols is undecidable [22,23]. Pushing the boundary from regular to a larger class of stream constraints can be useful for more effective synthesis methods.
## 2 Syntax and semantics

The semantics of constraint automata is defined as a relation over timed data streams [3], which are pairs, each consisting of a non-decreasing stream of time stamps and a stream of observed (exchanged) data items. The primary significance of time streams is the proper alignment of their respective data streams, by allowing “temporal gaps” during which no data is observed. For convenience, we drop the time stream and model protocols as relations over streams of data, augmented by a special symbol that designates “no-data” item.

We first define the abstract behavior of a protocol C. Fix an infinite set X of variables, and fix a non-empty set of user-data Data $\supseteq \{0\}$ that contains a datum 0. Consider the data domain $D = Data \cup \{*\}$ of data stream items, where we use the “no-data” symbol $*$ $\in D \setminus Data$ to denote the absence of data. We model the a single execution of protocol C as a function

$$ \theta : X \to D^N \qquad (1) $$

that maps every variable $x \in X$ to a function $\theta(x) : N \to D$ that represents a stream of data at location $x$. We call $\theta$ a data stream tuple (over $X$ and $D$). For all $n \in N$ and all $x \in X$, the value $\theta(x)(n) \in D$ is the data that we observe at location $x$ and time step $n$. If $\theta(x)(n) = *$, we say that no data is observed at $x$ in step $n$ (i.e., we may view $\theta$ as a partial map $N \times X \to Data$). The behavior of protocol C consists of the set

$$ \mathcal{L}(C) \subseteq (D^N)^X \qquad (2) $$

of all possible executions of C, called the accepted language of C. We can think of accepted language $\mathcal{L}(C)$ as a relation over data streams. In this paper, we study protocols that are defined as a stream constraint:

**Definition 1 (Stream constraints).** A stream constraint $\phi$ is an expression generated by the following grammar

$$ \begin{aligned} \phi &::= \bot | t_0 \doteq t_1 | \phi_0 \wedge \phi_1 | \neg \phi | \exists x \phi | \Box \phi \\ t &::= x | \mathbf{d} | t' \end{aligned} $$

where $x \in X$ is a variable, $d \in D$ is a datum, and $t$ is a stream term.

We use the following standard syntactic sugar: $\top = \neg \bot$, $\phi_0 \lor \phi_1 = \neg(\neg \phi_0 \land \neg \phi_1)$, $\diamond \phi = \neg \Box \neg \phi$, $\neg(t_1 \doteq t_2) = (t_1 \not\doteq t_2)$, $(t_1 \doteq t_2 \land \dots \land t_{n-1} \doteq t_n) = (t_1 \doteq \dots \doteq t_n)$, $t^{(0)} = t$, and $t^{(k+1)} = (t^{(k)})'$, for all $k \ge 0$. Following Rutten [25], we call $t^{(k)}$, $k \ge 0$, the k-th derivative of term $t$.

We interpret a stream constraint as a constraint over streams of data in $D^N$. For a datum $d \in D$, $\mathbf{d}$ is the constant stream defined as $\mathbf{d}(n) = d$, for all $n \in N$. The operator $(-)'$, called stream derivative, drops the head of the stream and is defined as $\sigma'(n) = \sigma(n + 1)$, for all $n \in N$ and $\sigma \in D^N$. Streams can be related by $\doteq$ that expresses equality of their heads: $x \doteq y$ iff $x(0) = y(0)$, for all
$x, y \in D^N$. The modal operator $\Box$ allows us to express that a stream constraint holds after applying any number of derivatives to all variables. For example, $\Box(x \doteq y)$ iff $x^{(k)}(0) = y^{(k)}(0)$, for all $k \in \mathbb{N}$ and $x, y \in D^N$. Stream constraints can be composed via conjunction $\wedge$, or negated via negation $\neg$. Streams can be hidden via existential quantification $\exists$.

Each stream term $t$ evaluates to a data stream in $D^N$. Let $\theta: X \to D^N$ be a data stream tuple. We extend the domain of $\theta$ from the set of variables $X$ to the set of terms $T \supseteq X$ as follows: we define $\theta: T \to D^N$ via $\theta(d) = d$ and $\theta(t') = \theta(t)'$, for all $d \in D$ and terms $t \in T$.

Next, we interpret a stream constraint $\phi$ as a relation over streams.

**Definition 2 (Semantics).** The language $\mathcal{L}(\phi) \subseteq (D^N)^X$ of a stream constraint $\phi$ over variables $X$ and data domain $D$ is defined as

1. $\mathcal{L}(\bot) = \emptyset$;

2. $\mathcal{L}(t_0 \doteq t_1) = \{\theta: X \to D^N \mid \theta(t_0)(0) = \theta(t_1)(0)\}$;

3. $\mathcal{L}(\phi_0 \wedge \phi_1) = \mathcal{L}(\phi_0) \cap \mathcal{L}(\phi_1)$;

4. $\mathcal{L}(\neg\phi) = (D^N)^X \setminus \mathcal{L}(\phi)$;

5. $\mathcal{L}(\exists x\phi) = \{\theta: X \to D^N \mid \theta[x \mapsto \sigma] \in \mathcal{L}(\phi), \text{ for some } \sigma \in D^N\}$;

6. $\mathcal{L}(\Box\phi) = \{\theta: X \to D^N \mid \theta^{(k)} \in \mathcal{L}(\phi), \text{ for all } k \ge 0\}$,

where $\theta[x \mapsto \sigma]: X \to D^N$ is defined as $\theta[x \mapsto \sigma](x) = \sigma$ and $\theta[x \mapsto \sigma](y) = \theta(y)$, for all $y \in X \setminus \{x\}$; and $\theta^{(k)}: X \to D^N$ is defined as $\theta^{(k)}(x) = \theta(x^{(k)})$, for all $x \in X$.

Let $\phi$ and $\psi$ be two stream constraints and $\theta: X \to D^N$ a data stream tuple. We say that $\theta$ satisfies $\phi$ (and write $\theta \models \phi$), whenever $\theta \in \mathcal{L}(\phi)$. We say that $\phi$ implies $\psi$ (and write $\phi \models \psi$), whenever $\mathcal{L}(\phi) \subseteq \mathcal{L}(\psi)$. We call $\phi$ and $\psi$ equivalent (and write $\phi \equiv \psi$), whenever $\mathcal{L}(\phi) = \mathcal{L}(\psi)$.

**Example 1.** One of the simplest stream constraints is sync$(a, b)$, which is defined as $\Box(a \doteq b)$. Constraint sync$(a, b)$ encodes that the data streams at $a$ and $b$ are equal: $\theta(a)(k) = \theta(b)(k)$, for all $k \in \mathbb{N}$ and all $\theta \in (D^N)^X$. Therefore, sync$(a, b)$ synchronizes the data flow observed at ports $a$ and $b$.

Conjunction $\wedge$ and existential quantification $\exists$ provide natural operators for composition and abstraction for stream constraints. For example, the composition sync$(a, b) \wedge$ sync$(b, c)$ synchronizes ports $a$, $b$, and $c$. Hiding port $b$ yields $\exists b(\text{sync}(a, b) \wedge \text{sync}(b, c))$, which is equivalent to sync$(a, c)$. $\Delta$

**Example 2.** Recall that $x^{(k)}$, for $k \ge 0$, is the $k$-th derivative of $x$. We can express that a stream $x$ is periodic via the stream constraint $\Box(x^{(k)} \doteq x)$, for some $k \ge 1$. For $k = 1$, stream $x$ is constant, like $\mathbf{0}$ and $\mathbf{*}$. $\Delta$

**Example 3.** The stream constraint `fifo$(a, b, m)$` defined as $m \doteq \mathbf{*} \wedge \Box((a \doteq m' \doteq \mathbf{0} \wedge b \doteq m \doteq \mathbf{*}) \vee (a \doteq m' \doteq \mathbf{*} \wedge b \doteq m \doteq \mathbf{0}) \vee (a \doteq b \doteq \mathbf{*} \wedge m' \doteq m))$ models a 1-place buffer with input location $a$, output location $b$, and memory location $m$ that can be full ($m \doteq \mathbf{0}$) or empty ($m \doteq \mathbf{*}$). $\Delta$

**Example 4.** Recall that $\mathbf{*}$ models absence of data. Stream constraint $\Box\diamond(a \neq \mathbf{*})$ expresses that always eventually we observe some datum at $a$. A constraint of such form can be used to define fairness. $\Delta$
## 3 Regular constraints

We identify a subclass of stream constraints that naturally correspond to constraint automata. We first introduce some notation.

To denote that a string $s$ occurs as a substring in a stream constraint $\phi$ or a stream term $t$, we write $s \in \phi$ or $s \in t$, respectively.

Every stream constraint $\phi$ admits a set free($\phi$) $\subseteq X$ of free variables, defined inductively via free($\bot$) = $\emptyset$, free($t_0$ $\doteq$ $t_1$) = {$x \in X \mid x \in t_0$ or $x \in t_1$}, free($\phi_0$ $\wedge$ $\phi_1$) = free($\phi_0$) $\cup$ free($\phi_1$), free($\neg \phi$) = free($\Box \phi$) = free($\phi$), and free($\exists x \phi$) = free($\phi$) $\setminus$ {$x$}.

For every variable $x \in X$, we define the degree of $x$ in $\phi$ as

$$ \deg_x(\phi) = \max(\{-1\} \cup \{k \ge 0 \mid x^{(k)} \in \phi\}), $$

and the degree of $\phi$ as $\deg(\phi) = \max_{x \in X} \deg_x(\phi)$. Note that for $x \notin \phi$ we have $\deg_x(\phi) = -1$. For $k \ge 0$, we write free$^k(\phi) = \{x \in \text{free}(\phi) \mid \deg_x(\phi) = k\}$ for the set of all free variables of $\phi$ of degree $k$.

We call a variable $x$ of degree zero in $\phi$ a port variable and write $P(\phi) = \text{free}^0(\phi)$ for the set of port variables of $\phi$. We call a variable $x$ of degree one or higher in $\phi$ a memory variable and write $M(\phi) = \bigcup_{k \ge 1} \text{free}^k(\phi)$ for the set of memory variables of $\phi$.

**Definition 3 (Regular).** A stream constraint $\phi$ is regular if and only if $\phi = \psi_0 \wedge \Box \psi$, such that $\Box \notin \psi_0 \wedge \psi$ and $\deg_x(\psi_0) < \deg_x(\psi) \le 1$, for all $x \in X$.

For a regular stream constraint $\phi = \psi_0 \wedge \Box \psi$, we refer to $\psi_0$ as the initial condition of $\phi$ and we refer to $\psi$ as the invariant of $\phi$. Stream constraints sync$(a, b)$ and fifo$(a, b, m)$ in Examples 1 and 3 are regular stream constraints.

A regular stream constraint $\phi$ has an operational interpretation in terms of a labeled transition system $[[\phi]]$. States of the transition system consist of maps $q : M(\phi) \to D$ that assign data to memory locations, and its labels consist of maps $\alpha : P(\phi) \to D$ that assign data to ports. We write $Q(\phi)$ for the set of states of $\phi$ and $A(\phi)$ for the set of labels of $\phi$.

**Definition 4 (Operational semantics).** The operational semantics $[[\phi]]$ of a regular stream constraint $\phi = \psi_0 \wedge \Box \psi$ consists of a labeled transition system $(Q(\phi), A(\phi), \to, Q_0)$, with set of states $Q(\phi)$, set of labels $A(\phi)$, set of transitions $\to = \{(q_\phi(\theta), q_\phi(\theta'), \alpha_\phi(\theta)) \mid \theta \in \mathcal{L}(\psi)\}$, and set of initial states $Q_0 = \{q_\phi(\theta) \mid \theta \in \mathcal{L}(\psi_0 \wedge \psi)\}$, where

1. $q_\phi(\theta) : M(\phi) \to D$ is defined as $q_\phi(\theta)(x) = \theta(x)(0)$, for $x \in M(\phi)$; and

2. $\alpha_\phi(\theta) : P(\phi) \to D$ is defined as $\alpha_\phi(\theta)(x) = \theta(x)(0)$, for $x \in P(\phi)$.

and $\theta'$ is defined as $\theta'(x)(n) = \theta(x)(n+1)$, for all $x \in X$ and $n \in \mathbb{N}$.

**Example 5.** Consider the regular stream constraint `fifo$(a, b, m)$` from Example 3. Note that in this example, the set of ports equals free$^0$(`fifo`)$= \{a, b\}$ and the set of memory locations equals free$^1$(`PIO`) $= \{m\}$. The semantics of `PIO$(a, b, m)$` over the trivial data domain $D = \{0, *\}$ consists of 4 transitions:
<figure><img src="image_2.png" /><figcaption>Fig. 1. Semantics of `fifo(a, b, m)` over the trivial data domain `{0, *}`.</figcaption></figure>

1. `([m ↦ *], [m ↦ 0], [a ↦ 0, b ↦ *])`;

2. `([m ↦ 0], [m ↦ *], [a ↦ *, b ↦ 0]);` and

3. `([m ↦ d], [m ↦ d], [a ↦ *, b ↦ *]),` for every $d \in \{*0\}$.

Figure 1 shows the semantics of `fifo` over the trivial data domain. $\Delta$

Equivalent stream constraints do not necessarily have the same operational semantics. We are, therefore, interested in operational equivalence of constraints:

**Definition 5 (Operational equivalence).** *Stream constraints $\phi$ and $\psi$ are operationally equivalent ($\phi \simeq \psi$) iff $\phi \equiv \psi$ and free$^k(\phi) = \text{free}^k(\psi)$, for $k \ge 0$.*

*Example 6.* Let $\phi$ be a stream constraint, let $t$ be a term and let $x \notin t$ be a variable that does not occur in $t$. Then, we have $\exists x (x \doteq t \land \phi) \equiv \phi[t/x]$, where $\phi[t/x]$ is obtained from $\phi$ by substituting $t$ for every free occurrence of $x$. Observe that $\exists x (x \doteq t \land \phi)$ and $\phi[t/x]$ may admit different sets of free variables: if $\phi$ is just $\top$ and $t$ is a variable $y$, the equivalence amounts to $\exists x (x \doteq y) \equiv \top$. To ensure that the free variables coincide, we can add the equality $t \doteq t$ and obtain the operational equivalence $\exists x (x \doteq t \land \phi) \simeq \phi[t/x] \land t \doteq t$. $\Delta$

Operational equivalence of stream constraints $\phi$ and $\psi$ implies that their operational semantics are identical, i.e., $[\phi] = [\psi]$. It is possible to introduce weaker equivalences by, for example, demanding that $[\phi]$ and $[\psi]$ are only weakly bisimilar. Such weaker equivalence offer more room for simplification of stream constraints than operational equivalence does. As our work does not need this generality, we leave the study of such weaker equivalences as future work.

The most important operations on stream constraints are composition (`&`) and hiding (`$\exists$`). The following result shows that regular stream constraints are closed under conjunction and existential quantification of degree zero variables.

**Theorem 1.** For all stream constraints $\phi$ and $\psi$ and variables $x$, we have

1. $\Box\phi \wedge \Box\psi \equiv \Box(\phi \wedge \psi)$; and

2. $\exists x \Box\phi \equiv \Box\exists x\phi$, whenever $\deg_x(\phi) \le 0$ and $\Box \notin \phi$.

*Proof.* For assertion 1, $\mathcal{L}(\Box\phi \wedge \Box\psi) = \{\theta \in (D^N)^X \mid \forall k \ge 0 : \theta^{(k)} \models \phi \wedge \psi\} = \mathcal{L}(\Box(\phi \wedge \psi))$ shows that $\Box\phi \wedge \Box\psi \equiv \Box(\phi \wedge \psi)$.

For assertion 2, suppose that $\deg_x(\phi) \le 0$ and $\Box \notin \phi$. We show that $\theta \in \mathcal{L}(\Box\exists x\phi)$ if and only if $\theta \in \mathcal{L}(\exists x\Box\phi)$, for all $\theta \in (D^N)^X$. By Definition 2, this equivalence can be written as

$$ \theta^{(k)}[x \mapsto \mu_k] \models \phi \iff (\theta[x \mapsto \sigma])^{(k)} \models \phi, \quad (3) $$
for all $k \ge 0$, $\sigma \in D^N$, and $\mu_k \in D^N$ such that $\mu_k(0) = \sigma^{(k)}(0)$.

To prove Equation (3), we proceed by induction on the length of $\phi$:

*Case 1 ($\phi := \perp$):* Since $\mathcal{L}(\perp) = \emptyset$, Equation (3) holds trivially.

*Case 2 ($\phi := t_0 \doteq t_1$):* Observe that, since $\deg_x(\phi) \le 0$, for all terms $t$, we have $x \in t$ iff $t = x$. We conclude Equation (3) from $\mu_k(0) = \sigma^{(k)}(0)$ and

$$ \theta^{(k)}[x \mapsto \mu_k](t)(0) = \begin{cases} \mu_k(0) & \text{if } t = x \\ \theta^{(k)}(t)(0) & \text{if } t \neq x \end{cases} = (\theta[x \mapsto \sigma])^{(k)}(t)(0). $$

*Case 3 ($\phi := \psi_0 \wedge \psi_1$):* By the induction hypothesis, Equation (3) holds for $\psi_0$ and $\psi_1$. By conjunction of Equation (3), we conclude Equation (3) for $\phi$.

*Case 4 ($\phi := \neg \psi$):* By the induction hypothesis, Equation (3) holds for $\psi$. By contraposition of Equation (3), we conclude Equation (3) for $\phi$.

*Case 5 ($\phi := \exists y \psi$):* If $y = x$, then $x \notin \text{free}(\phi)$ and both sides in Equation (3) are equivalent to $\theta^{(k)} \models \phi$. Hence, Equation (3) holds for $y = x$. Suppose $y \neq x$. Then, $\theta^{(k)}[x \mapsto \mu_k] \models \phi$ is equivalent to $(\theta[y \mapsto \tau])^{(k)}[x \mapsto \mu_k] \models \psi$, for some $\tau \in D^N$. Applying the induction hypothesis for $\theta$ equal to $\theta[y \mapsto \tau]$, we conclude that $\theta^{(k)}[x \mapsto \mu_k] \models \phi$ is equivalent to $(\theta[y \mapsto \tau][x \mapsto \sigma])^{(k)} \models \psi$, for some $\tau \in D^N$. Since $y \neq x$, we conclude that Equation (3) holds.

We conclude that the claim holds for all $\phi$ with $\deg_x(\phi) \le 0$ and $\square \notin \phi$. $\square$

# 4 Reflexive constraints

Conjunction of stream constraints is a simple syntactic composition operator with clear semantics: a data stream tuple $\theta$ satisfies a conjunction $\phi_0 \wedge \phi_1$ if and only if $\theta$ satisfies both $\phi_0$ and $\phi_1$. In view of the semantics of regular stream constraints in Definition 2, it is less obvious how $[[\phi_0 \wedge \phi_1]]$ relates to $[[\phi_0]]$ and $[[\phi_1]]$. The following result characterizes their relation when no memory is shared.

**Theorem 2.** Let $\phi_0$ and $\phi_1$ be regular stream constraints such that $\text{free}(\phi_0) \cap \text{free}(\phi_1) \subseteq P(\phi_0 \wedge \phi_1)$, and let $(q_i, q'_i, \alpha_i) \in Q(\phi_i)^2 \times A(\phi_i)$, for $i \in \{0, 1\}$. The following are equivalent:

1. $q_0 \xrightarrow{\alpha_0} q'_0$ in $[[\phi_0]]$, $q_1 \xrightarrow{\alpha_1} q'_1$ in $[[\phi_1]]$, and $\alpha_0|_{P(\phi_1)} = \alpha_1|_{P(\phi_0)}$;

2. $q_0 \cup q_1 \xrightarrow{\alpha_0 \cup \alpha_1} q'_0 \cup q'_1$ in $[[\phi_0 \wedge \phi_1]]$,

where $|$ is restriction of maps, and $\cup$ is union of maps.

*Proof.* Write $\phi_i = \psi_{i0} \wedge \Box \psi_i$, with $\Box \notin \psi_{i0} \wedge \psi_i$ and $\deg_x(\psi_{i0}) < \deg_x(\psi_i) \le 1$, for all $x \in X$. Then, $\text{free}^k(\phi_i) = \text{free}^k(\psi_i)$, for all $i, k \in \{0, 1\}$.

Suppose that assertion 1 holds. By Definition 2, we find, for all $i \in \{0, 1\}$, some $\theta_i \in \mathcal{L}(\psi_i)$ such that $q_i = q_{\phi_i}(\theta_i)$, $q'_i = q_{\phi_i}(\theta'_i)$, and $\alpha_i = \alpha_{\phi_i}(\theta_i)$. Define $\theta: X \to D^N$ by $\theta(x) = \theta_i(x)$, if $x \in \text{free}(\phi_i)$, and $\theta(x) = \ast$, otherwise. Since $\text{free}(\phi_0) \cap \text{free}(\phi_1) \subseteq P(\phi_0 \wedge \phi_1)$ and $\alpha_0|_{P(\phi_1)} = \alpha_1|_{P(\phi_0)}$, we have that $\theta_0(x) = \theta_1(x)$, for all $x \in \text{free}(\phi_0) \cap \text{free}(\phi_1)$. Hence, $\theta$ is well-defined. By construction, $\theta \models \psi_0$ and $\theta \models \psi_1$. By Definition 2, we have $\theta \models \psi_0 \wedge \psi_1$. By Theorem 1, we have
$\phi_0 \wedge \phi_1 = \psi_{00} \wedge \psi_{10} \wedge \Box(\psi_0 \wedge \psi_1)$. Since $q_0 \cup q_1 = q_{\phi_0 \wedge \phi_1}(\theta)$, $q'_0 \cup q'_1 = q_{\phi_0 \wedge \phi_1}(\theta')$, and $\alpha_0 \cup \alpha_1 = \alpha_{\phi_0 \wedge \phi_1}(\theta)$, we conclude assertion 2.

Suppose that assertion 2 holds. We find some $\theta \in \mathcal{L}(\psi_0 \wedge \psi_1)$, such that $q_0 \cup q_1 = q_\theta$, $q'_0 \cup q'_1 = q_{\theta'}$, and $\alpha_0 \cup \alpha_1 = \alpha_\theta$. Then, we conclude assertion 1, for $q_i = q_{\phi_i}(\theta)$, $q'_i = q_{\phi_i}(\theta')$, and $\alpha_i = \alpha_{\phi_i}(\theta)$. $\square$

Stream constraints $\phi_0$ and $\phi_1$ without shared variables (free($\phi_0$) $\cap$ free($\phi_1$) = $\emptyset$) seem completely independent. However, Theorem 2 shows that their composition $\phi_0 \wedge \phi_1$ admits a transition only if $\phi_0$ and $\phi_1$ admit respective local transitions $(q_0, q'_0, \alpha_0)$ and $(q_1, q'_1, \alpha_1)$, such that $\alpha_0|_{P(\phi_1)} = \alpha_1|_{P(\phi_0)}$. Since $\phi_0$ and $\phi_1$ do not share variables, the latter condition on $\alpha_0$ and $\alpha_1$ is trivially satisfied. Still, for one protocol $\phi_i$, with $i \in \{0,1\}$, to make progress in the composition $\phi_0 \wedge \phi_1$, constraint $\phi_{1-i}$ must admit an idling transition.

To allow such independent progress, we assume that $\phi_{1-i}$ admits an idling transition $(q, q, \tau)$, where $\tau$ is the silent label over $P(\phi_{1-i})$. The silent label over a set of ports $P \subseteq X$ is the map $\tau: P \to D$ that maps $x \in P$ to $* \in D$. If such idling transitions are available in every state of $\phi_1$, we say that $\phi_1$ is reflexive:

**Definition 6 (Reflexive).** A stream constraint $\phi$ is reflexive if and only if $q \xrightarrow{\tau} q$ in $[[\phi]]$, for all $q \in Q(\phi)$.

For regular constraints, we can define reflexiveness also syntactically, for which we need some notation. For a variable $x \in X$ and an integer $k \in \mathbb{N} \cup \{-1\}$, we define the predicate $x^{\dagger}_k$ (pronounced: “$x$ is blocked at step $k$”) as follows:

$$x^{\dagger}_k := (x^{(k)} \doteq x^{(k-1)}), \quad \text{with } x^{(k)} \doteq \ast, \text{ for all } k < 0.$$

Predicate $x^{\dagger}_{-1} \equiv \top$ is trivially true. Predicate $x^{\dagger}_0 \equiv (x \doteq \ast)$ means that we observe no data flow at port $x$. Predicate $x^{\dagger}_1 \equiv (x' \doteq x)$ means that the data in memory variable $x$ remains the same.

We now provide a syntactic equivalent of Definition 6 for regular constraints.

**Lemma 1.** A regular stream constraint $\phi = \psi_0 \wedge \Box \psi$ is reflexive if and only if $\bigwedge_{x \in X} x^{\dagger d(x)} \models \psi$, where $d(x) = \deg_x(\phi)$, for all $x \in X$.

*Proof.* Since $d(x) = -1$, for all but finitely many $x \in X$, the stream constraint $\bigwedge_{x \in X} x^{\dagger d(x)}$ is well-defined. By definition, $\bigwedge_{x \in X} x^{\dagger d(x)} \models \psi$ if and only if, for all $q \in Q(\phi)$, there exists some $\theta \in \mathcal{L}(\psi)$, such that $q_\theta = q_{\theta'} = q$ and $\alpha_\theta = \tau$. $\square$

*Example 7.* The stream constraint $\text{sync}(a, b) := \Box(a \doteq b)$ from Example 1 is reflexive, because $\bigwedge_{x \in X} x^{\dagger d(x)} = a \doteq \ast \wedge b \doteq \ast$ implies $a \doteq b$. The stream constraint *fifo* from Example 3 is reflexive, because $\bigwedge_{x \in X} x^{\dagger d(x)} = a \doteq \ast \wedge b \doteq \ast \wedge m' \doteq m$ is one of the clauses of *fifo*. $\triangle$

Theorem 2 suggests a composition operator $\times$ on labeled transition systems, satisfying $[[\phi_0]] \times [[\phi_1]] = [[\phi_0 \wedge \phi_1]]$. For reflexive constraints $\phi_0$ and $\phi_1$, composition $\times$ simulates composition of constraint automata [6]. Constraint automata also feature a hiding operator that naturally corresponds to existential quantification $\exists$ for stream constraints. We leave a full formal comparison between stream constraints and constraint automata as future work.
# 5 Rule-based form

The commandification algorithm developed by Jongmans accepts only conjunc-
tions of literals [14]. To apply commandification to the invariant $\psi$ of an arbitrary
regular stream constraint $\psi_0 \wedge \Box \psi$, we can first transform $\psi$ into disjunctive nor-
mal form (DNF). However, the number of clauses in the disjunctive normal form
may be exponential in the length of the constraint. In this section, we introduce
an alternative to the disjunctive normal form that prevents such exponential
blow up, for a strictly larger class of stream constraints. Our main observation is
that the clauses of the disjunctive normal form may contain many symmetries,
in the sense that we may generate all clauses from a set of stream constraints $R$,
called a set of rules. A rule is a stream constraint $\rho$, such that $\deg(\rho) \le 1$ and
$\Box \notin \rho$.

**Definition 7 (Rule-based form).** A reflexive stream constraint $\phi$ is in rule-based form iff $\phi$ equals

$$ \mathrm{rbf}(R) = \bigwedge_{x \in \mathrm{free}(R)} x^{\dagger d(x)} \lor \bigvee_{\rho \in R: x \in \mathrm{free}(\rho)} \rho \quad (4) $$

with $R$ a finite set of rules, $\mathrm{free}(R) = \bigcup_{\rho \in R} \mathrm{free}(\rho)$, and $d(x) = \max_{\rho \in R} \deg_x(\rho)$. A stream constraint $\phi$ is defined by $R$ iff $\phi \simeq \mathrm{rbf}(R)$.

We apply the rule-based form to the invariant of regular constraints, via $\psi_0 \wedge \Box \mathrm{rbf}(R)$, for some degree zero stream constraint $\psi_0$ and set of rules $R$. Intuitively, $R$ remains smaller than the DNF of $\mathrm{rbf}(R)$ under composition.

**Example 8.** $\psi \simeq \mathrm{rbf}(\{\psi\})$, for all reflexive stream constraints $\psi$, with $\deg(\psi) \le 1$ and $\Box \notin \psi$. Hence, Example 7 shows $\mathrm{sync}(a, b) = \Box (a \doteq b) \simeq \Box \mathrm{rbf}(\{a \doteq b\})$. $\Delta$

**Example 9.** The stream constraint $\mathrm{lossy}(a, b) := \Box \mathrm{rbf}(\{a \doteq a, a \doteq b\})$ is equivalent to $\Box (b \doteq * \lor a \doteq b)$. Note that $\Box \mathrm{rbf}(\{\top, a \doteq b\}) \simeq \Box \mathrm{rbf}(\{a \doteq b\}) \simeq \mathrm{sync}(a, b)$. Hence, rules $a \doteq a$ and $\top$ are very different. $\Delta$

**Example 10.** The set of rules that define a stream constraint is not unique. Consider the stream constraint $\mathrm{fifo}$ from Example 3. On the one hand, we have $\mathrm{fifo}(a, b, m) \simeq m \doteq * \wedge \Box \mathrm{rbf}(\{\varphi, \psi\})$, where $\varphi \simeq a \doteq m' \doteq \mathbf{0} \wedge m \doteq *$ models the action that puts data in the buffer and $\psi \simeq m' \doteq * \wedge b \doteq m \doteq \mathbf{0}$ models the action that takes data out of the buffer. On the other hand, we have $\mathrm{fifo}(a, b, m) \simeq m \doteq * \wedge \Box \mathrm{rbf}(\{a \doteq m' \doteq \mathbf{0} \wedge b \doteq m \doteq *, a \doteq m' \doteq * \wedge b \doteq m \doteq \mathbf{0}\})$. $\Delta$

**Example 11.** Rule-based forms are an alternative to disjunctive normal forms. Consider the reflexive constraint $\phi := \bigvee_{i=1}^n \rho_i$ in DNF for which the first conjunctive clause $\rho_1$ is equivalent to $\bigwedge_{x \in \mathrm{free}(\phi)} x^{\dagger d(x)}$, with $d(x) = \deg_x(\phi)$. By adding equalities of the form $x \doteq x$, we assume without loss of generality that $\mathrm{free}(\rho_i) = \mathrm{free}(\phi)$, for all $2 \le i \le n$. For $R = \{\rho_i | 2 \le i \le n\}$, it follows from

$$ \mathrm{rbf}(R) \equiv \bigwedge_{x \in \mathrm{free}(R)} \left( x^{\dagger d(x)} \lor \bigvee_{\rho \in R} \rho \right) \equiv \left( \bigwedge_{x \in \mathrm{free}(\phi)} x^{\dagger d(x)} \right) \lor \bigvee_{\rho \in R} \rho \equiv \phi \quad (5) $$
that $\phi$ is defined by the set $R$.

△

Definition 7 presents the rule-based form as a conjunctive normal form. The following result computes the disjunctive normal form of rbf($R$).

**Lemma 2.** For every set of rules $R$, we have

$$ \mathrm{rbf}(R) \simeq \mathrm{dnf}(R) := \bigvee_{T \subseteq R} \bigwedge_{\rho \in T} \bigwedge_{x \in \mathrm{free}(R) \setminus \mathrm{free}(T)} x^{\dagger}_{d(x)}. $$

*Proof.* Let $x \in X$ be arbitrary. By construction, we have $\deg_x(\mathrm{dnf}(R)) \le \max_{\rho \in R} \deg_x(\rho)$. Since $d(x) = \max_{\rho \in R} \deg_x(\rho)$, the clause for $T = \emptyset$ shows that $\deg_x(\mathrm{dnf}(R)) \ge d(x)$. By Lemma 4, $\deg_x(\mathrm{rbf}(R)) = \deg_x(\mathrm{dnf}(R))$, for all $x \in X$. Hence, $\mathrm{free}^k(\mathrm{rbf}(R)) = \mathrm{free}^k(\mathrm{dnf}(R))$, for all $k \ge 0$.

Next, we show that $\mathrm{rbf}(R) \models \mathrm{dnf}(R)$. Let $\theta \in \mathcal{L}(\mathrm{rbf}(R))$. We find, for every $x \in \mathrm{free}(R)$, some rule $\rho_x \in R$, such that $\theta \models \rho$ and $x \in \mathrm{free}(\rho)$. Now, define $T_\theta := \{\rho_x \mid x \in \mathrm{free}(R) \text{ and } \theta \notin \mathcal{L}(x^{\dagger}_{d(x)})\}$. By construction, $\theta \models \rho_x$, for every $\rho_x \in T_\theta$. If $x \in \mathrm{free}(R)$ and $\theta \notin \mathcal{L}(x^{\dagger}_{d(x)})$, then $\rho_x \in T_\theta$ and $x \in \mathrm{free}(\rho_x) \subseteq \mathrm{free}(T_\theta)$. By contraposition, we conclude that $\theta \models x^{\dagger}_{d(x)}$, for all $x \in \mathrm{free}(R) \setminus \mathrm{free}(T_\theta)$. Hence, $\theta \models \mathrm{dnf}(R)$, and $\mathcal{L}(\mathrm{rbf}(R)) \subseteq \mathcal{L}(\mathrm{dnf}(R))$.

Finally, we show that $\mathrm{dnf}(R) \models \mathrm{rbf}(R)$. Let $\theta \in \mathcal{L}(\mathrm{dnf}(R))$. By definition of $\mathrm{dnf}(R)$, we find some $T \subseteq R$ with $\theta \models \rho$, for all $\rho \in T$, and $\theta \models x^{\dagger}_{d(x)}$, for all $x \in \mathrm{free}(R) \setminus \mathrm{free}(T)$. Suppose that $x \in \mathrm{free}(R)$ and $\theta \not\models x^{\dagger}_{d(x)}$. Since $\theta \models x^{\dagger}_{d(x)}$, for all $x \in \mathrm{free}(R) \setminus \mathrm{free}(T)$, we find by contraposition that $x \in \mathrm{free}(T)$. Hence, we find some $\psi \in T$ with $x \in \mathrm{free}(\psi)$. Since $\theta \models \rho$, for all $\rho \in T$, we find that $\theta \models \psi$. Hence, $\theta \models \mathrm{rbf}(R)$ and we conclude that $\mathrm{rbf}(R) \simeq \mathrm{dnf}(R)$. □

# 6 Composition

We express conjunction of stream constraints in terms of their defining sets of rules. That is, for two sets of rules $R_0$ and $R_1$, we define the composition $R_0 \wedge R_1$ of $R_0$ and $R_1$, such that $\mathrm{rbf}(R_0 \wedge R_1) \simeq \mathrm{rbf}(R_0) \wedge \mathrm{rbf}(R_1)$. If $R_0$ and $R_1$ do not share any variable (i.e., $\mathrm{free}(R_0) \cap \mathrm{free}(R_1) = \emptyset$), composition $R_0 \wedge R_1$ is given by the union $R_0 \cup R_1$. In this section, we define the composition $R_0 \wedge R_1$ of $R_0$ and $R_1$ for $\mathrm{free}(R_0) \cap \mathrm{free}(R_1) \neq \emptyset$.

In view of Example 11, consider the normal form $\mathrm{dnf}(R_0 \wedge R_1)$. Since $\mathrm{dnf}(R_0 \wedge R_1)$ equals $\mathrm{dnf}(R_0) \wedge \mathrm{dnf}(R_1)$, it suffices to characterize the set of clauses of $\mathrm{dnf}(R_0) \wedge \mathrm{dnf}(R_1)$. Every such clause is a conjunction of a clause in $\mathrm{dnf}(R_0)$ and a clause in $\mathrm{dnf}(R_1)$. Lemma 2 shows that the clauses of $\mathrm{dnf}(R_i)$ correspond to subsets $T_i$ of $R_i$, for all $i \in \{0, 1\}$. Not every pair of subsets $T_0 \subseteq R_0$ and $T_1 \subseteq R_1$ yields a clause of $\mathrm{dnf}(R_0) \wedge \mathrm{dnf}(R_1)$, but only if $S = T_0 \cup T_1$ is synchronous:

**Definition 8 (Synchronous).** A synchronous set over sets of rules $R_0$ and $R_1$ is a subset $S \subseteq R_0 \cup R_1$, with $\mathrm{free}(S) \cap \mathrm{free}(R_i) \subseteq \mathrm{free}(S \cap R_i)$, for all $i \in \{0, 1\}$.

*Example 12.* For any integer $i \ge 1$, let $\varphi_i := a_i \doteq m'_i \doteq \mathbf{0} \wedge m_i \doteq \ast$ and $\psi_i := m'_i \doteq \ast \wedge a_{i+1} \doteq m_i \doteq \mathbf{0}$ be the two rules that define $\mathrm{fifof}(a_i, a_{i+1}, m_i)$, from
Example 10. The synchronous sets consist of exactly those sets $S \subseteq \{\varphi_1, \psi_1\} \cup \{\varphi_2, \psi_2\}$ that satisfy $\psi_1 \in S$ iff $\varphi_2 \in S$. That is, the synchronous sets are given by $\emptyset, \{\varphi_1\}, \{\psi_2\}, \{\psi_1, \varphi_2\}, \{\varphi_1, \psi_1, \varphi_2\}, \{\psi_1, \varphi_2, \psi_2\}, \{\varphi_1, \psi_1, \varphi_2, \psi_2\}$. $\Delta$

Next, we recognize symmetries in the collection of synchronous sets. We can construct every synchronous set as a union of *irreducible* synchronous subsets:

**Definition 9 (Irreducibility).** A non-empty synchronous set $\emptyset \neq S \subseteq R_0 \cup R_1$ is irreducible if and only if $S = S_0 \cup S_1$ implies $S = S_0$ or $S = S_1$, for all synchronous subsets $S_0, S_1 \subseteq R_0 \cup R_1$.

Example 13. Let $R_0$ and $R_1$ be sets of rules, and let $\rho \in R_0$ be a rule, such that $\text{free}(\rho) \cap \text{free}(R_1) = \emptyset$. We show that $\{\rho\}$ is irreducible synchronous. Since $\text{free}(\{\rho\}) \cap \text{free}(R_0) = \text{free}(\rho) = \text{free}(\{\rho\} \cap R_0)$ and $\text{free}(\{\rho\}) \cap \text{free}(R_1) = \emptyset \subseteq \text{free}(\{\rho\} \cap R_1)$, we conclude that $\{\rho\}$ is synchronous. Suppose $\{\rho\} = S_0 \cup S_1$. Then, $\rho \in S_i$, for some $i \in \{0, 1\}$. Hence, $\{\rho\} \subseteq S_i \subseteq \{\rho\}$, which shows that $S_i = \{\rho\}$. We conclude that $\{\rho\}$ is irreducible synchronous in $R_0 \cup R_1$. $\Delta$

Example 14. Consider $\varphi_i$ and $\psi_i$, for $i \in \{1, 2\}$, from Example 12. The irreducible synchronous sets of $\{\varphi_1, \psi_1\} \cup \{\varphi_2, \psi_2\}$ are $\{\varphi_1\}$, $\{\psi_2\}$, and $\{\psi_1, \varphi_2\}$. $\Delta$

**Definition 10 (Composition).** The composition of sets of rules $R_0$ and $R_1$ is $R_0 \wedge R_1 := \bigwedge_{\rho \in S} \rho \mid S \subseteq R_0 \cup R_1$ irreducible synchronous sets.

Example 15. Let $R_0$ and $R_1$ be sets of rules, with $\text{free}(R_0) \cap \text{free}(R_1) = \emptyset$. By Example 13, we find that $\{\rho\} \subseteq R_0 \cup R_1$, for all $\rho \in R_0 \cup R_1$, is irreducible synchronous. Hence, every synchronous set $S \subseteq R_0 \cup R_1$, with $|S| \ge 2$, is reducible. Therefore, $S \subseteq R_0 \cup R_1$ is irreducible synchronous if and only if $S = \{\rho\}$, for some $\rho \in R_0 \cup R_1$. We conclude that $R_0 \wedge R_1 = R_0 \cup R_1$. Consequently, $\emptyset$ is a (unique) identity element with respect to composition $\wedge$ of sets of rules. $\Delta$

To show that the composition of sets of rules coincides with conjunction of stream constraints, we need the following result that shows that every non-empty synchronous set can be covered by irreducible synchronous sets.

**Lemma 3.** Let $R_0$ and $R_1$ be sets of rules, and let $S \subseteq R_0 \cup R_1$ be a non-empty synchronous set. Then, $S = \cup_{i=1}^n S_i$, where $S_i \subseteq R_0 \cup R_1$, for $1 \le i \le n$, is irreducible synchronous.

*Proof.* We prove the lemma by induction on the size $|S|$ of $S$. For the base case, suppose that $|S| = 1$. We show that $S$ is irreducible synchronous, which provides a trivial covering. Suppose that $S = S_0 \cup S_1$, for some synchronous sets $S_0, S_1 \subseteq R_0 \cup R_1$. Since, $|S| = 1$, we have $S \subseteq S_i \subseteq S$, for some $i \in \{0, 1\}$. Hence, $S = S_i$, and $S$ is irreducible. We conclude that the lemma holds, for $|S| = 1$.

For the induction step, suppose that $|S| = k > 1$, and suppose that the lemma holds, for $|S| < k$. If $S$ is irreducible, we find a trivial covering of $S$. If $S$ is reducible, we find $S = S_0 \cup S_1$, where $S_0 \neq S \neq S_1$ are synchronous sets in $R_0 \cup R_1$. Since $|S_i| < |S|$, for $i \in \{0, 1\}$, we find by the hypothesis that $S_i = \cup_{j=1}^{n_i} S_{ij}$. Hence, $S = S_0 \cup S_1 = \cup_{i=0}^1 \cup_{j=1}^{n_i} S_{ij}$. We conclude that the lemma holds, for $|S| = k$. By induction on $|S|$, we conclude the lemma. $\square$
**Lemma 4.** $\deg_x(\text{rfb}(R)) = \max_{\rho \in R} \deg_x(\rho)$, for all sets of rules $R$ and $x \in X$.

*Proof.* For any set of rules $R$ and $y \in X$, we have

$$ \deg_y(\text{rfb}(R)) = \max_{x \in \text{free}(R)} \max(\deg_y(x^{\dagger d(x)}), \max_{\rho \in R: x \in \text{free}(\rho)} \deg_y(\rho)). $$

Note that $\deg_y(x^{\dagger d(x)}) = d(y)$, if $y = x$, and $\deg_y(x^{\dagger d(x)}) = -1$, otherwise. Since $d(y) = \max_{\rho \in R} \deg_y(\rho)$, we have $\deg_y(\text{rfb}(R)) = \max_{\rho \in R} \deg_y(\rho)$. $\square$

**Theorem 3.** $\text{rfb}(R_0 \wedge R_1) \simeq \text{rfb}(R_0) \wedge \text{rfb}(R_1)$, for all sets of rules $R_0$ and $R_1$.

*Proof.* By Lemma 4 and Definition 10, $\deg_x(\text{rfb}(R_0 \wedge R_1)) = \deg_x(\text{rfb}(R_0) \wedge \text{rfb}(R_1))$, for all $x \in X$. Hence, $\text{free}^k(\text{rfb}(R_0 \wedge R_1)) = \text{free}^k(\text{rfb}(R_0) \wedge \text{rfb}(R_1))$, for all $k \ge 0$.

Next, we show $\text{rfb}(R_0) \wedge \text{rfb}(R_1) \models \text{rfb}(R_0 \wedge R_1)$. Let $\theta \in \mathcal{L}(\text{rfb}(R_0) \wedge \text{rfb}(R_1))$. By Definition 7, we must show that for every $x \in \text{free}(R_0 \wedge R_1)$ there exists some $\rho_x \in R_0 \wedge R_1$ such that $x \in \text{free}(\rho_x)$ and either $\theta \models x^{\dagger d(x)}$ or $\theta \models \rho_x$. Hence, suppose that $\theta \notin \mathcal{L}(x^{\dagger d(x)})$, for some variable $x \in \text{free}(R_0 \wedge R_1)$. Since $\text{free}(R_0 \wedge R_1) = \text{free}(R_0) \cup \text{free}(R_1)$ and $\theta \models \text{free}(R_0) \wedge \text{free}(R_1)$, we find from Definition 7 some $\psi \in R_0 \cup R_1$, with $\theta \models \psi$ and $x \in \text{free}(\psi)$. We now show that there exists an irreducible synchronous set $S \subseteq R_0 \cup R_1$, such that, for $\rho_x := \bigwedge_{\rho \in S} \rho$, we have $\theta \models \rho_x$ and $x \in \text{free}(\rho_x)$. By repeated application of Definition 8, we construct a finite sequence

$$ \{\psi\} = S_0 \subsetneq \dots \subsetneq S_n, $$

such that $S_n \subseteq R_0 \cup R_1$ is synchronous, and $\theta \models \bigwedge_{\rho \in S_n} \rho$. Suppose $S_k \subseteq R_0 \cup R_1$, for $k \ge 1$, is not synchronous. By Definition 8, there exists some $i \in \{0, 1\}$ and a variable $x \in \text{free}(S_k) \cap \text{free}(R_i)$, such that $x \notin \text{free}(S_k \cap R_i)$. Since $x \in \text{free}(R_i)$, we have $R_i^x := \{\rho \in R_i | x \in \text{free}(\rho)\} \neq \emptyset$. Since $\theta \models \text{rfb}(R_i)$, there exists some $\psi_k \in R_i^x$ such that $\theta \models \psi_k$. Now define $S_{k+1} := S_k \cup \{\psi_k\}$. Since $x \notin \text{free}(S_k \cap R_i)$ and $x \in \text{free}(S_{k+1} \cap R_i)$, we have a strict inclusion $S_k \subseteq S_{k+1}$. Due to these strict inclusions, we have, for $k \ge |R_0 \cup R_1|$, that $S_k = R_0 \cup R_1$, which is trivially synchronous in $R_0 \cup R_1$. Therefore, our sequence $S_0 \subsetneq \dots$ of inclusions terminates, from which we conclude the existence of $S_n$. By Lemma 3, we find some irreducible synchronous set $S \subseteq S_n$, such that $\psi \in S$. We conclude that $\rho_x := \bigwedge_{\rho \in S} \rho \in R_0 \wedge R_1$ satisfies $\theta \models \rho_x$ and $x \in \text{free}(\psi) \subseteq \text{free}(S) = \text{free}(\rho_x)$. By Definition 7, we have $\theta \models \text{rfb}(R_0 \wedge R_1)$, and $\text{rfb}(R_0) \wedge \text{rfb}(R_1) \models \text{rfb}(R_0 \wedge R_1)$.

Finally, we prove that $\text{rfb}(R_0 \wedge R_1) \models \text{rfb}(R_0) \wedge \text{rfb}(R_1)$. Let $\theta \in \mathcal{L}(\text{rfb}(R_0 \wedge R_1))$. We show that $\theta \models \text{rfb}(R_i)$, for all $i \in \{0, 1\}$. By Definition 7, we must show that for every $i \in \{0, 1\}$ and every $x \in \text{free}(R_i)$ there exists some $\rho \in R_i$ such that $x \in \text{free}(\rho)$ and either $\theta \models x^{\dagger d(x)}$ or $\theta \models \rho$. Hence, let $i \in \{0, 1\}$ and $x \in \text{free}(R_i)$ be arbitrary, and suppose that $\theta \notin \mathcal{L}(x^{\dagger d(x)})$. Since $\text{free}(R_i) \subseteq \text{free}(R_0 \wedge R_1)$, it follows from our assumption $\theta \models \text{rfb}(R_0 \wedge R_1)$ that $\theta \models \bigwedge_{\rho \in S} \rho$, for some irreducible synchronous set $S \subseteq R_0 \cup R_1$ satisfying $x \in \text{free}(S)$. Since $S \subseteq R_0 \cup R_1$ synchronous, we find that $x \in \text{free}(S) \cap \text{free}(R_i) = \text{free}(S \cap R_i)$. Hence, we find some $\rho \in S \cap R_i$, such that $\theta \models \rho$ and $x \in \text{free}(\rho)$. By Definition 7, we conclude that $\theta \models \text{rfb}(R_i)$, for all $i \in \{0, 1\}$. Therefore, $\text{rfb}(R_0 \wedge R_1) \simeq \text{rfb}(R_0) \wedge \text{rfb}(R_1)$. $\square$
<figure><img src="image_3.png" /><figcaption>Fig. 2. Hypergraph representations of $\bigwedge_{i=1}^2 \text{fifo}(a_i, a_{i+1}, m_i)$.</figcaption></figure>

**Example 16.** Let $\varphi_i$ and $\psi_i$, for $i \ge 1$, be the rules from Example 12. By Example 14, the composition $\text{fifo}_2 := \bigwedge_{i=1}^2 \text{fifo}(a_i, a_{i+1}, m_i)$ is defined by the set of rules $\{\varphi_1, \psi_1 \wedge \varphi_2, \psi_2\}$.<fnref n="1" /> To compute a set of rules that defines the composition, it is not efficient to enumerate all (exponentially many) synchronous subsets of $R_0 \cup R_1$ and remove all reducible sets. Our tools use an algorithm based on hypergraph transformations to compute the irreducible synchronous sets. The details of this algorithm fall outside the scope of this paper. Figure 2 shows a graphical representation of composition $\text{fifo}_2$, using hypergraphs. These hypergraphs consist of sets of hyperedges $(x, F)$, where $x$ is a variable and $F$ is a set of rules. Each hyperedge $(x, F)$ in a hypergraph corresponds to a disjunction $x \dagger_{d(x)} \lor \bigvee_{\rho \in F} \rho$ of the rule-based form in Definition 7. $\triangle$

# 7 Complexity

In the worst case, composition $R_0 \wedge R_1$ of arbitrary sets of rules $R_0$ and $R_1$ may consists of $|R_0| \times |R_1|$ rules. However, if $R_0$ and $R_1$ are simple, the size of the composition is bounded by $|R_0| + |R_1|$.

**Definition 11 (Simple).** A set $R$ of rules is simple if and only if $\text{free}(\rho) \cap \text{free}(\rho') \cap P(\text{rbf}(R)) \neq \emptyset$ implies $\rho = \rho'$, for every $\rho, \rho' \in R$.

**Example 17.** By Example 10, the invariant of $\text{fifo}(a, b, m)$ is defined by $R := \{a \doteq m' \doteq \mathbf{0} \wedge m \doteq \mathbf{*}, m' \doteq \mathbf{*} \wedge b \doteq m \doteq \mathbf{0}\}$ as well as $R' := \{a \doteq m' \doteq \mathbf{0} \wedge b \doteq m \doteq \mathbf{*}, a \doteq m' \doteq \mathbf{*} \wedge b \doteq m \doteq \mathbf{0}\}$. The set $R$ is simple, while $R'$ is not. $\triangle$

<footnote n="1">¹ The rules for the composition of two `fifo` stream constraints has striking similarities with synchronous region decomposition developed by Proença et al. [24]. Indeed, $\varphi_1$, $\psi_1 \wedge \varphi_2$, and $\psi_2$ correspond to the synchronous regions in the composition of two buffers. Therefore, rule-based composition generalizes synchronous region decomposition that has been used as a basis for generation of parallel code [15].</footnote>
*Proof.* From Lemmas 3 and 6, we find that the irreducible synchronous subsets partition $R_0 \cup R_1$. We conclude that $|R_0 \wedge R_1| \le |R_0| + |R_1|$. We now show that $R_0 \wedge R_1$ is simple. Let $\rho_0$ and $\rho_1$ be rules in $R_0 \wedge R_1$, with free($\rho_0$) $\cap$ free($\rho_1$) $\cap$ $P_{01} \ne \emptyset$, where $P_{01} = P(\text{rbf}(R_0 \cup R_1))$. By Definition 10, we find, for all $i \in \{0,1\}$, an irreducible synchronous set $S_i$, such that $\rho_i = \bigwedge_{\psi \in S_i} \psi$. Since free($\rho_0$)$\cap$free($\rho_1$)$\cap$ $P_{01} \ne \emptyset$ and free($\rho_i$) = free($S_i$), for all $i \in \{0,1\}$, we find some $x \in$ free($S_0$)$\cap$free($S_1$)$\cap$ $P_{01}$. Suppose that $x \in$ free($R_j$), for some $j \in \{0,1\}$. Since $S_0$ and $S_1$ are synchronous sets, we have $x \in$ free($S_i$)$\cap$free($R_j$) $\subseteq$ free($S_i \cap R_j$), for all $i \in \{0,1\}$. We find, for all $i \in \{0,1\}$, some $\psi_i \in S_i \cap R_j$, such that $x \in$ free($\psi_i$). Hence, free($\psi_0$) $\cap$ free($\psi_1$) $\cap$ $P_{01} \ne \emptyset$, and since $R_j$ is simple, we conclude that $\psi_0 = \psi_1$. Therefore, $S_0 \cap S_1 \ne \emptyset$, and Lemma 6 shows that $S_0 = S_1$ and $\rho_0 = \rho_1$. We conclude that $R_0 \wedge R_1$ is simple. $\square$

The number of clauses in the disjunctive normal form of direct compositions of $k$ `fifo` constraints grows exponentially in $k$. This typical pattern of a sequence of queues manifests itself in many other constructions, which causes serious scalability problems (cf., the benchmarks for ‘Alternator$_k$’ in [17, Section 7.2]). However, Theorem 4 shows that rule-based composition of $k$ `fifo` constraints does not suffer from scalability issues: by Example 17, the `fifo` constraint can be defined by a simple set of rules. The result in Theorem 4, therefore, promises (exponential) improvement over the classical constraint automaton representation.

Unfortunately, it seems impossible to define any arbitrary stream constraint by a simple set of rules. Therefore, the rule-based form may still blow up for certain stream constraints. It seems, however, possible to recognize even more symmetries (cf., the queue-optimization in [16]) to avoid explosion and obtain comparable compilation and execution performance for these stream constraints.

# 8 Abstraction

We now study how existential quantification of stream constraints operates on its defining set of rules.

**Definition 12 (Abstraction).** *Hiding a variable $x$ in a set of rules $R$ yields $\exists x R := \{\exists x \rho \mid \rho \in R\}$.*

Unfortunately, $\exists x R$ does not always define $\exists x \phi$, for a stream constraint $\phi$ defined by a set of rules $R$. The following result shows that $\exists x R$ defines $\exists x \phi$ if and only if $\text{rbf}(\exists x R) \models \exists x \text{rbf}(R)$. In this case, we call variable $x$ *hidable* in $R$.

It is non-trivial to find a defining set of rules for $\exists x \phi$, if $x$ is not hidable in $R$, and we leave this as future work.

**Theorem 5.** Let $R$ be a set of rules, and let $x \in X$ be a variable. Then, $\exists x \text{rbf}(R) \simeq \text{rbf}(\exists x R)$ if and only if $\text{rbf}(\exists x R) \models \exists x \text{rbf}(R)$.

*Proof.* Trivially, $\exists x \text{rbf}(R) \simeq \text{rbf}(\exists x R)$ implies $\text{rbf}(\exists x R) \models \exists x \text{rbf}(R)$. Conversely, suppose that $\text{rbf}(\exists x R) \models \exists x \text{rbf}(R)$. From Lemma 2, it follows that
$\exists x \text{rfb}(R) \equiv \exists x \text{dnf}(R)$. Since existential quantification distributes over disjunction and $\exists x \phi \wedge \psi \models \exists x \phi \wedge \exists x \psi$, for all stream constraints $\phi$ and $\psi$, we find

$$ \exists x \text{dnf}(R) \models \bigvee_{S \subseteq R} \bigwedge_{\rho \in S} \exists x \rho \wedge \bigwedge_{x \neq y \in \text{free}(R) \setminus \text{free}(S)} y^{\dagger}_{d(y)} \equiv \text{dnf}(\exists x R). $$

By Lemma 2, we have $\exists x \text{rfb}(R) \models \text{rfb}(\exists x R)$, and by assumption $\exists x \text{rfb}(R) \equiv \text{rfb}(\exists x R)$. Using Lemma 4, we have $\text{deg}_y(\exists x \text{rfb}(R)) = \max_{\rho \in R} \text{deg}_y(\exists x \rho) = \text{deg}_y(\text{rfb}(\exists x R))$, for every variable $y$. We conclude $\exists x \text{rfb}(R) \simeq \text{rfb}(\exists x R)$. $\square$

**Example 18.** Suppose $\text{Data} = \{0, 1\}$, which means that the data domain equals $D = \{0, 1, *\}$. Let $\mathbf{1}$ be the constant stream defined as $\mathbf{1}(n) = 1$, for all $n \in \mathbb{N}$. For $i \in \{0, 1\}$, consider the set of rules $R_i = \{x = x, x = y_i = \mathbf{i}\}$. Observe that $\{x = x, x = y_i = \mathbf{i}\} \subseteq R_0 \cup R_1$ is synchronous, for all $i \in \{0, 1\}$. Hence, $x = y_i = \mathbf{i} \in R_0 \wedge R_1$, for all $i \in \{0, 1\}$. However, for $\theta = [y_0 \mapsto \mathbf{0}, y_1 \mapsto \mathbf{1}]$, we have $\theta \models \bigwedge_{i \in \{0, 1\}} \exists x (x = y_i = i)$, while $\exists x \bigwedge_{i \in \{0, 1\}} x = y_i = i \equiv \perp$. Thus, variable $x$ is not hidable from $R_0 \wedge R_1$. $\triangle$

# 9 Application

In on-going work, we applied the rule-based form to compile protocols (in the form of Reo connectors) into executable code. Reo is an exogenous coordination language that models protocols as graph-like structures [1,2]. We recently developed a textual version of Reo, which we use to design non-trivial protocols [11]. An example of such non-trivial protocol is the Alternator$_k$, where $k \ge 2$ is an integer. Figure 3(a) shows a graphical representation of the Alternator$_k$ protocol.

Intuitively, the behavior of the alternator protocol is as follows: The nodes $P_1, \dots, P_k$ accept data from the environment. Node $C$ offers data to the environment. All other nodes are internal and do not interact with the environment. In the first step of the protocol, the Alternator$_k$ waits until the environment is ready to offer data at all nodes $P_1, \dots, P_k$ and is ready to accept data from node $C$. Only then, the Alternator$_k$ transfers the data from $P_k$ to $C$ via a synchronous channel, and puts the data from $P_i$ in the $i$-th *fifo* channel, for all $i < k$. The behavior of a synchronous channel is defined by the *sync* stream constraint in Example 1. Each *fifo* channel has buffer capacity of one, and its behavior is defined by the *fifo* stream constraint from Example 3. In subsequent steps, the environment can one-by-one retrieve the data from the *fifo* channel buffers, until they are all empty. Then, the protocol cycles back to its initial configuration, and repeats its behavior. For more details on the Reo language and its semantics, we refer to [1,2].

As mentioned in the introduction, Jongmans developed a compiler based on constraint automata [17]. The otherwise stimulating benchmarks presented in [17] show that Jongmans’ compiler still suffers from state-space explosion. Figure 3(b) shows the compilation time of the Alternator$_k$ protocol for Jongmans’ compiler and ours. Clearly, the compilation time improved drastically and went from exponential in $k$ to almost linear in $k$.
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** Graphical representation (a) of the Alternator$_k$ protocol in [17], for $2 \le k \le 500$, and its compilation time (b). The dotted red line is produced by the Jongmans’ compiler (and corresponds to [17, Fig 11(a)]), and the solid blue line is our compiler.</figcaption></figure>

Every `fifo` channel in the Alternator$_k$, except the first, either accepts data from the environment or accepts data from the previous `fifo` channel. This choice is made by the internal node at the input of each `fifo` channel. Unfortunately, the behavior of such nodes is not defined in terms of a simple set of rules. Consequently, we cannot readily apply Theorem 4 to conclude that the number of rules depends only linearly on $k$. However, it turns out that Alternator$_k$ can be defined using only $k$ rules: one rule for filling the buffers of all `fifo` channels, plus $k-1$ rules, one for taking data out of the buffer of each of the $k-1$ `fifo` channels. This observation explains why our compiler drastically improves upon Jongmans’ compiler.

# 10 Conclusion

We introduce (regular) stream constraints as an alternative to constraint automata that does not suffer from state space explosions. We define the rule-based form for stream constraints, and we express composition and abstraction of constraints in terms of their rule-based forms. For simple sets of rules, composition of rule-based forms does not suffer from ‘transition space explosions’ either.

We have experimented with a new compiler for protocols using our rule-based form, which avoids the scalability problems of state- and transition-space explosions of previous automata-based tools. Our approach still leaves the possibility for transition space explosion for non-simple sets of rules. In the future, we intend to study symmetries in stream constraints that are not defined by simple sets of rules. The queue-optimization of Jongmans serves as a good source of inspiration for exploiting symmetries [16].

The results in this paper are purely theoretical. In on-going work, we show practical implications of our results by developing a compiler based on stream
constraints. Such a compiler requires an extension to the current theory on
stream constraints: we did not compute the abstraction $∃xR$ on sets of rules $R$
wherein variable $x$ is not hidable. Example 11 indicates the existence of situations
where we can compute $∃xR$ even if $x$ is not hidable, a topic which we leave as
future work.

**Acknowledgements** The authors thank Benjamin Lion for his help in developing a rule-based compiler and for generating Figure 3(b).

References

1. Arbab, F.: Reo: a channel-based coordination model for component composition. Mathematical Structures in Computer Science 14(3), 329–366 (2004), https://doi.org/10.1017/S0960129504004153

2. Arbab, F.: Puff, the magic protocol. In: Agha, G., Danvy, O., Meseguer, J. (eds.) Formal Modeling: Actors, Open Systems, Biological Systems - Essays Dedicated to Carolyn Talcott on the Occasion of Her 70th Birthday. Lecture Notes in Computer Science, vol. 7000, pp. 169–206. Springer (2011), https://doi.org/10.1007/978-3-642-24933-4_9

3. Arbab, F., Rutten, J.J.M.M.: A coinductive calculus of component connectors. In: Wirsing, M., Pattinson, D., Hennicker, R. (eds.) Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002, Frauenchiemsee, Germany, September 24-27, 2002, Revised Selected Papers. Lecture Notes in Computer Science, vol. 2755, pp. 34–55. Springer (2002), https://doi.org/10.1007/978-3-540-40020-2_2

4. Baier, C., Blechmann, T., Klein, J., Klüppelholz, S.: A uniform framework for modeling and verifying components and connectors. In: Field, J., Vasconcelos, V.T. (eds.) Coordination Models and Languages, 11th International Conference, COORDINATION 2009, Lisboa, Portugal, June 9-12, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5521, pp. 247–267. Springer (2009), https://doi.org/10.1007/978-3-642-02053-7_13

5. Baier, C., Clarke, E.M., Hartonas-Garmhausen, V., Kwiatkowska, M.Z., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) Automata, Languages and Programming, 24th International Colloquium, ICALP’97, Bologna, Italy, 7-11 July 1997, Proceedings. Lecture Notes in Computer Science, vol. 1256, pp. 430–440. Springer (1997), https://doi.org/10.1007/3-540-63165-8_199

6. Baier, C., Sirjani, M., Arbab, F., Rutten, J.J.M.M.: Modeling component connectors in reo by constraint automata. Sci. Comput. Program. 61(2), 75–113 (2006), https://doi.org/10.1016/j.scico.2005.10.008

7. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Computers 35(8), 677–691 (1986), https://doi.org/10.1109/TC.1986.1676819

8. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10^20 states and beyond. Inf. Comput. 98(2), 142–170 (1992), https://doi.org/10.1016/0890-5401(92)90017-A

9. Clarke, D., Proença, J., Lazovik, A., Arbab, F.: Channel-based coordination via constraint satisfaction. Sci. Comput. Program. 76(8), 681–710 (2011), https://doi.org/10.1016/j.scico.2010.05.004
10. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L. (eds.): All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350. Springer (2007), https://doi.org/10.1007/978-3-540-71999-1

11. Dokter, K., Arbab, F.: Treo: Textual syntax of reo connectors. In: Proc. of MeTRiD 2018 (2018), to appear

12. Ehlers, R.: Minimising deterministic büchi automata precisely using SAT solving. In: Strichman, O., Szeider, S. (eds.) Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture Notes in Computer Science, vol. 6175, pp. 326-332. Springer (2010), https://doi.org/10.1007/978-3-642-14186-7_28

13. Jongmans, S.T.Q.: Automata-theoretic protocol programming. Ph.D. thesis, Centrum Wiskunde & Informatica (CWI), Faculty of Science, Leiden University (2016), http://hdl.handle.net/1887/38223

14. Jongmans, S.T.Q., Arbab, F.: Prdk: Protocol programming with automata. In: Chechik, M., Raskin, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9636, pp. 547-552. Springer (2016), https://doi.org/10.1007/978-3-662-49674-9_33

15. Jongmans, S.T.Q., Arbab, F.: Centralized coordination vs. partially-distributed coordination with reo and constraint automata. Science of Computer Programming (2017), http://www.sciencedirect.com/science/article/pii/S0167642317301259

16. Jongmans, S.T.Q., Halle, S., Arbab, F.: Automata-based optimization of interaction protocols for scalable multicore platforms. In: eva Kühn, Pugliese, R. (eds.) Coordination Models and Languages - 16th IFIP WG 6.1 International Conference, COORDINATION 2014, Held as Part of the 9th International Federated Conferences on Distributed Computing Techniques, DisCoTec 2014, Berlin, Germany, June 3-5, 2014, Proceedings. Lecture Notes in Computer Science, vol. 8459, pp. 65-82. Springer (2014), https://doi.org/10.1007/978-3-662-43376-8_5

17. Jongmans, S.T.Q., Kappé, T., Arbab, F.: Constraint automata with memory cells and their composition. Sci. Comput. Program. 146, 50-86 (2017), https://doi.org/10.1016/j.scico.2017.03.006

18. Kemper, S.: Sat-based verification for timed component connectors. Sci. Comput. Program. 77(7-8), 779-798 (2012), https://doi.org/10.1016/j.scico.2011.02.003

19. Klüppelholz, S.: Verification of Branching-Time and Alternating-Time Properties for Exogenous Coordination Models. Ph.D. thesis, Dresden University of Technology (2012), http://www.qucosa.de/recherche/frontdoor/?tx_slubopus4frontend[id]=8621

20. Kwiatkowska, M.Z., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Inf. Comput. 205(7), 1027-1077 (2007), https://doi.org/10.1016/j.ic.2007.01.004

21. Murata, T.: Petri nets: Properties, analysis and applications. Proceedings of the IEEE 77(4), 541-580 (1989)

22. Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming
Languages, Austin, Texas, USA, January 11-13, 1989. pp. 179-190. ACM Press (1989), http://doi.acm.org/10.1145/75277.75293

23. Pnueli, A., Rosner, R.: Distributed reactive systems are hard to synthesize. In: 31st Annual Symposium on Foundations of Computer Science, St. Louis, Missouri, USA, October 22-24, 1990, Volume II. pp. 746-757. IEEE Computer Society (1990), https://doi.org/10.1109/FSCS.1990.89597

24. Proença, J., Clarke, D., de Vink, E.P., Arbab, F.: Dreams: a framework for distributed synchronous coordination. In: Ossowski, S., Lecca, P. (eds.) Proceedings of the ACM Symposium on Applied Computing, SAC 2012, Riva, Trento, Italy, March 26-30, 2012. pp. 1510-1515. ACM (2012), http://doi.acm.org/10.1145/2245276.2232017

25. Rutten, J.J.M.M.: Elements of stream calculus (an extensive exercise in coinduction). Electr. Notes Theor. Comput. Sci. 45, 358-423 (2001), https://doi.org/10.1016/S1571-0661(04)80972-1