11institutetext:  CWI, Amsterdam, The Netherlands
11email<EMAIL_ADDRESS>22institutetext: Leiden University, Leiden, The
Netherlands
22email<EMAIL_ADDRESS>33institutetext: SRI International, CA, USA
33email<EMAIL_ADDRESS>
# Runtime Composition Of Systems of Interacting Cyber-Physical Components

Benjamin Lion 11 Farhad Arbab 1122 Carolyn Talcott 33

###### Abstract

We introduce a transition system based specification of cyber-physical systems
whose semantics is compositional with respect to a family of algebraic
products. We give sufficient conditions for execution of a product to be
correctly implemented by a lazy expansion of the product construction. The
transition system algebra is implemented in the Maude rewriting logic system,
and we report a simple case study illustrating compositional specification.

##  1 Introduction

We model a cyber-physical system as a pair consisting of an interface and a
behavior. We call such pairs components. The interface is a set of events and
the behavior is a set of infinite sequences of observations called Timed-Event
Stream (TES), where an observation is a pair of a set of events from the
interface and a time stamp.

In previous work, we define a family of parametrized binary products to
compose components. The parameters of a product consist of a composability
relation on TESs, which says which pairs of TESs can compose, and a
composition function, which says how two TESs compose to form a new TES. For
instance, the synchronous product of two components with shared events
composes pairs of TESs, one from each component behavior, such that shared
events occur at the same time. The resulting TES interleaves observations from
a pair of composable TESs. In order to bridge the gap between a denotational
model and an operational model, we give a co-inductive definition of
composability relations on TESs as a lift of composability relations on
observations. Such locally defined relations provide a step-wise mechanism to
check whether two TESs are composable.

In this paper, we give an operational mechanism to specify components by
transition systems labeled with observations, called TES transition systems.
Different TES transition systems may denote the same component, as a component
is oblivious to internal non-determinism of the machinery that manifests its
behavior.

As for components, we introduce a family of parametrized algebraic products on
TES transition systems. The parameter here is a composability relation on
observations, and each transition in the product is the result of the
composition of a pair of transitions with composable labels. We show that the
TES transition system component semantics is compositional with respect to
such products, i.e., the component resulting from the product of two TES
transition systems is equal to the product of the components resulting from
each TES transition system. On components, the composability relation is co-
inductively lifted from observations to TESs, and the composition function is
set union on observations and interleaving on streams.

Because the composability relation on observations is a step-wise operation,
it may lead to deadlock states in the product TES transition system, i.e.,
states with no outgoing transitions. We call two TES transition systems
_compatible_ with respect to a composability relation on observations if, for
every reachable pair of states, there is at least one pair of transitions
whose pair of labels is composable. We give some sufficient conditions for TES
transition systems to be compatible, and show that if two TES transitions
system are compatible, then their product can be done lazily, i.e., step by
step at runtime.

To carry out experiments, we have implemented TES transition systems in the
Maude rewriting logic system. We use this implementation to analyze properties
of the behavior of a set of self-sorting robots. In this example, each robot
has a unique integer identifier, its own battery, and interacts with others
via a shared grid. Robots, batteries, and grids are all modeled as TES
transition systems. We add a set of _swap_ protocols each of which coordinates
a pair of robots to swap their positions when a robot faces another robot with
a lower identifier and a higher $x$-axis coordinate. We analyze the resulting
system by querying if a robot can reach its sorted configuration on the grid.
The interaction among all TES transition systems is captured by a suitable
composability relation on observations.

Our work has the following benefits. First, performing lazy composition keeps
the representation of an interacting system small. Second, step-wise runtime
composition renders our runtime framework modular, where run-time replacement
of individual components becomes possible (as long as the update complies with
some rules). Finally, the runtime framework more closely matches the
architecture of a distributed framework, where entities are physically
separated and no party may have access to the whole description of the entire
system.

##  2 Components in interaction

In [9], we give a unified semantic model to capture cyber and physical aspects
of processes as components and characterize their various types of
interactions as user-defined products in an algebraic framework. Moreover, we
show some general conditions for products on components to be associative,
commutative, and idempotent. In this section, we recall the basic definitions
of a component and product from [9], and introduce in Section 2.2 some
instances of product that suit our example in this paper.

#### Notations.

Given $\sigma:\mathbb{N}\to\Sigma$, let $\sigma[n]\in\Sigma^{n}$ be the finite
prefix of size $n$ of $\sigma$ and let $\sim_{n}$ be an equivalence relation
on $(\mathbb{N}\to\Sigma)\times(\mathbb{N}\to\Sigma)$ such that
$\sigma\sim_{n}\tau$ if and only if $\sigma[n]=\tau[n]$. Let $\mathit{FG}(L)$
be the set of _left factors_ of a set $L\subseteq\Sigma^{\omega}$, defined as
$\mathit{FG}(L)=\\{\sigma[n]\mid n\in\mathbb{N},\ \sigma\in L\\}$. We write
$\sigma^{(n)}$ for the $n$-th derivative of $\sigma$, i.e., the stream such
that $\sigma^{(n)}(i)=\sigma(n+i)$ for all $i\in\mathbb{N}$.

A timed-event stream $\sigma\in\mathit{TES}(E)$ over a set of events $E$ is an
infinite sequence of _observations_ , where an observation $\sigma(i)=(O,t)$
consists of a pair of a subset of events in $O\subseteq E$, called
_observable_ , and a positive real number $t\in\mathbb{R}_{+}$ as time stamp.
A timed-event stream (TES) has the additional properties that consecutive time
stamps are increasing and non-Zeno, i.e., for any TES $\sigma$ and any time
$t\in\mathbb{R}$, there exists an element $\sigma(i)=(O_{i},t_{i})$ in the
sequence such that $t<t_{i}$. We use $\sigma^{\prime}$ to denote the
derivative of the stream $\sigma$, such that $\sigma^{\prime}(i)=\sigma(i+1)$
for all $i\in\mathbb{N}$.

We recall the greatest post fixed point of a monotone operator, that we later
use as a definition scheme and as a proof principle. Let $X$ be any set and
let $\mathcal{P}(X)=\\{V\mid V\subseteq X\\}$ be the set of all its subsets.
If $\Psi:\mathcal{P}(X)\rightarrow\mathcal{P}(X)$ is a monotone operator, that
is, $R\subseteq S$ implies $\Psi(R)\subseteq\Psi(S)$ for all $R\subseteq X$
and $S\subseteq X$, then $\Psi$ has a greatest fixed point $P=\Psi(P)$
satisfying:

$P=\bigcup\\{R\mid R\subseteq\Psi(R)\\}$

This equality can be used as a proof principle: in order to prove that
$R\subseteq P$, for any $R\subseteq X$, it suffices to show that $R$ is a
post-fixed point of $\Psi$, that is, $R\subseteq\Psi(R)$.

###  2.1 Components

Components are the parts that forms cyber-physical systems. Therefore, a
component uniformly models both cyber and physical aspects through sequence of
observables.

######  Definition 1 (Component)

A _component_ $C=(E,L)$ is a pair of an _interface_ $E$, and a _behavior_
$L\subseteq\mathit{TES}(E)$. $\triangle$

The product of two components defines a new component whose behavior is
function of the behavior of both components, under some constraints. We call a
_composability relation_
$R(E_{1},E_{2})\subseteq\mathit{TES}(E_{1})\times\mathit{TES}(E_{2})$ such
constraint, and say that $(\sigma_{1},\sigma_{2})$ are two _composable_ TESs
if $(\sigma_{1},\sigma_{2})\in R(E_{1},E_{2})$. Furthermore, two TESs may then
compose to form a new TES. We call a _composition function_
$\oplus:\mathit{TES}(E_{1})\times\mathit{TES}(E_{2})\rightarrow\mathit{TES}(E_{1}\cup
E_{2})$ such function, and write $\sigma_{1}\oplus\sigma_{2}$ for the
composition of $\sigma_{1}$ and $\sigma_{2}$.

Let $C_{1}=(E_{1},L_{1})$ and $C_{2}=(E_{2},L_{2})$ be two components. Let
$R(E_{1},E_{2})$ be a composability relation and $\oplus$ be a composition
function.

######  Definition 2 (Product)

The _product_ of $C_{1}$ and $C_{2}$ under $(R,\oplus)$ is the component
$C=C_{1}\times_{(R,\oplus)}C_{2}=(E_{1}\cup E_{2},L)$ where

$\\{\sigma_{1}\oplus\sigma_{2}\mid\sigma_{1}\in L_{1},\sigma_{2}\in L_{2},\
(\sigma_{1},\sigma_{2})\in R(E_{1},E_{2})\\}$

$\triangle$

While the behaviors of a component are streams, it is natural to consider
termination of a component. We express a terminating behavior of component
$C=(E,L)$ as an element $\sigma\in L$ such that there exists $n\in\mathbb{N}$
with $\sigma^{(n)}\in\mathit{TES}(\emptyset)$. In other words, a terminating
behavior $\sigma$ is such that, starting from the $n$-th observation, all next
observations are empty.

Given a component $C$, we define $C^{*}$ to be the component that may
terminate after every sequence of observables. Formally, $C^{*}$ is the
component whose behavior is the prefix closure of $C$, i.e., the component
$C^{*}=(E,L^{*})$, where

$L^{*}=L\cup\\{\tau\mid\exists n\in\mathbb{N}.\exists\sigma\in L.\
\tau\sim_{n}\sigma,\ \tau^{(n)}\in\mathit{TES}(\emptyset)\\}$

In [9], we give a co-inductive definition for some $R$ and $\oplus$ given a
composability relation on observations, and a composition function on
observations. We use
$\kappa(E_{1},E_{2})\subseteq(\mathcal{P}(E_{1})\times\mathbb{R}_{+})\times(\mathcal{P}(E_{2})\times\mathbb{R}_{+})$
to range over composability relation on observations. Let $\kappa$ be a
parametric composability relation on observations, and let
$\Phi_{\kappa}(E_{1},E_{2})$ be such that, for any
$\mathcal{R}\subseteq\mathit{TES}(E_{1})\times\mathit{TES}(E_{2})$:

$\begin{array}[]{rl}\Phi_{\kappa}(E_{1},E_{2})(\mathcal{R})=\\{(\tau_{1},\tau_{2})\mid&(\tau_{1}(0),\tau_{2}(0))\in\kappa(E_{1},E_{2})\land\\\
&(\mathrm{pr}_{2}(\tau_{1})(0)=t_{1}\land\mathrm{pr}_{2}(\tau_{2})(0)=t_{2})\land\\\
&(t_{1}<t_{2}\land(\tau_{1}^{\prime},\tau_{2})\in\mathcal{R}\lor
t_{2}<t_{1}\land(\tau_{1},\tau_{2}^{\prime})\in\mathcal{R}\lor\\\ &\quad
t_{2}=t_{1}\land(\tau_{1}^{\prime},\tau_{2}^{\prime})\in\mathcal{R})\\}\end{array}$

The _lifting_ of $\kappa$ on TESs, written $[\kappa]$, is the parametrized
relation obtained by taking the greatest post fixed point of the function
$\Phi_{\kappa}(E_{1},E_{2})$ for arbitrary pair
$E_{1},E_{2}\subseteq\mathbb{E}$, i.e., the relation
$[\kappa](E_{1},E_{2})=\bigcup_{\mathcal{R}\subseteq\mathit{TES}(E_{1}){}\times\mathit{TES}(E_{2}){}}\\{\mathcal{R}\mid\mathcal{R}\subseteq\Phi_{\kappa}(E_{1},E_{2})(\mathcal{R})\\}$.

Then, let $\sqcap\subseteq\mathcal{P}(\mathbb{E})^{2}$ be a relation on
observables. We say that two observations are synchronous under $\sqcap$ if,
intuitively, the two following conditions hold:

  1. 1.

every observable that can compose (under $\sqcap$) with another observable
must occur simultaneously with one of its related observables; and

  2. 2.

only an observable that does not compose (under $\sqcap$) with any other
observable can happen before another observable, i.e., at a strictly lower
time.

To formalize the conditions above, we use the independence relation
$\mathit{ind}_{\sqcap}$ where $\mathit{ind}_{\sqcap}(X,Y)=\forall x\subseteq
X.\forall y\subseteq Y.(x,y)\not\in\sqcap$.

The _synchronous_ composability relation on observations
$\kappa^{\mathit{sync}}_{\sqcap}(E_{1},E_{2})$ is the smallest set such that,
for $O_{1},O_{1}^{\prime}\subseteq\mathcal{P}(E_{1})$ and
$O_{2},O_{2}^{\prime}\subseteq\mathcal{P}(E_{2})$:

  * •

if $(O_{1},O_{2})\in\sqcap$ and $\mathit{ind}_{\sqcap}(O_{1}^{\prime},E_{2})$
and $\mathit{ind}_{\sqcap}(E_{1},O_{2}^{\prime})$ then, for all time stamps
$t\in\mathbb{R}_{+}$, $((O_{1}\cup O_{1}^{\prime},t),(O_{2}\cup
O_{2}^{\prime},t))\in\kappa_{\sqcap}^{\mathit{sync}}(E_{1},E_{2})$.

  * •

if $\mathit{ind}_{\sqcap}(O_{1},E_{2})$ then for all $X_{2}\subseteq E_{2}$
and $t_{1}\leq t_{2}$,
$((O_{1},t_{1}),(X_{2},t_{2}))\in\kappa^{\mathit{sync}}_{\sqcap}(E_{1},E_{2})$.
Reciprocally, if $\mathit{ind}_{\sqcap}(E_{1},O_{2})$ then for all
$X_{1}\subseteq E_{1}$ and $t_{2}\leq t_{1}$,
$((X_{1},t_{1}),(O_{2},t_{2}))\in\kappa^{\mathit{sync}}_{\sqcap}(E_{1},E_{2})$;

Let $\bowtie$ be the product defined as $\bowtie\
=\times_{([\kappa_{\sqcap}^{\mathit{sync}}],[\cup])}$ where
$\sqcap=\\{(O,O)\mid O\subseteq\mathbb{E}\\}$ with $\mathbb{E}$ the universal
set of events. Intuitively, $\bowtie$ synchronizes all observations that
contain events shared by the interface of two components. We recall that the
composition $[\cup]$ of two TESs $\sigma_{1}$ and $\sigma_{2}$ is such that it
interleaves, in order, all observations with distinct time stamps, and takes
the union of two observations with the same time stamp, i.e., the _lifting_ of
set union $\cup$ to TESs, written $[\cup]$, is such that, for
$\sigma_{1},\sigma_{2}\in\mathit{TES}(\mathbb{E})$ where
$\sigma_{i}(0)=(O_{i},t_{i})$ with $i\in\\{1,2\\}$:

$\sigma_{1}[\cup]\sigma_{2}=\begin{cases}\langle\sigma_{1}(0)\rangle\cdot(\sigma_{1}^{\prime}[\cup]\sigma_{2})&\mathit{if}\
t_{1}<t_{2}\\\
\langle\sigma_{2}(0)\rangle\cdot(\sigma_{1}[\cup]\sigma_{2}^{\prime})&\mathit{if}\
t_{2}<t_{1}\\\ \langle(O_{1}\cup
O_{2},t_{1})\rangle\cdot(\sigma_{1}^{\prime}[\cup]\sigma_{2}^{\prime})&\mathit{otherwise}\end{cases}$

As a result of [9], $\bowtie$ is associative and commutative. Section 2.2
introduces a motivating example in which robots, roaming on a shared physical
medium, must coordinate to sort themselves. We define algebraically the system
consisting of 5 robots and a grid, to which we then add some coordinating
protocol components.

###  2.2 Self-sorting robots

Consider a robot component $R$, that moves on a grid and reads its position.
Its interface consists of the coordinates $(x,y)_{R}$ that it reads and the
direction $d_{R}$ of its moves, i.e., $E_{R}=\\{(x,y)_{R},d_{R}\mid
d\in\\{S,W,N,E\\},\ (x,y)\in\mathbb{R}_{+}\times\mathbb{R}_{+}\\}$. The robot
freely moves and observes its position at anytime, then its behavior is a
subset $L_{R}\subseteq\mathit{TES}(E_{R})$. We use $R$ to refer to an
arbitrary robot component with interface $E_{R}$.

We aim to model the physical constraints explicitly. Thus, the grid on which
the robot moves is another component. Its interface is parametrized by a set
$I$ of robot identifiers, and by a pair $(n,m)$ for its size on the $x$-axis
and $y$-axis respectively, i.e., $E_{G}(I,n,m)=\\{(x,y)_{R},d_{R}\mid
d\in\\{S,W,N,E\\},R\in I,(x,y)\in[1;n]\times[1;m]\\}$. The behavior of a grid
is a set $L_{G}\subseteq\mathit{TES}(E_{G})$ such that, for any $\sigma\in
L_{G}$ and for any element $\sigma(i)=(O_{i},t_{i})$, if $(x,y)_{R}\in O_{i}$
then $(x,y)_{R^{\prime}}\not\in O_{i}$ for every $R^{\prime}\not=R$: two
robots cannot share the same location. Note that the physics has some internal
constraints (no two robots can share the same cell) that no robot _a priori_
is aware of. Typically, the move of a robot coincides with a change of state
of the grid: if a robot $R$ is at position $(x,y)_{R}$ and does a move
$N_{R}$, then the next observable position for robot $R$ will be
$(x,y+1)_{R}$. We give in Example 1 an operational definition of the grid
component. We use $G(I,n,m)$ to refer to an arbitrary grid component with set
of events $E_{G}(I,n,m)$.

Figure 1 shows five robot instances, each of which has a unique and distinct
natural number assigned, positioned at an initial location on a grid. The goal
of the robots in this example is to move around on the grid such that they end
up in a final state where they line-up in the sorted order according to their
assigned numbers.

$R_{5}$$R_{4}$$R_{3}$$R_{2}$$R_{1}$

$\Rightarrow_{*}$

$R_{1}$$R_{2}$$R_{3}$$R_{4}$$R_{5}$

Figure 1: Initial state of the unsorted robots (left), and final state of the
sorted robots (right).

| $R_{1}$ | $R_{2}$ | $R_{3}$ | $R_{4}$ | $R_{5}$
---|---|---|---|---|---
$t_{1}$ | N | - | - | - | -
$t_{2}$ | W | - | - | - | -
$t_{3}$ | $(3;1)$ | - | - | - | -
$...$ | $...$ | $...$ | $...$ | $...$ | $...$

| $R_{1}$ | $R_{2}$ | $R_{3}$ | $R_{4}$ | $R_{5}$
---|---|---|---|---|---
$t_{1}$ | N | - | - | - | -
$t_{2}$ | W | E | N | - | -
$t_{3}$ | S | $(4;0)$ | E | - | -
$...$ | $...$ | $...$ | $...$ | $...$ | $...$

| $R_{1}$ | $R_{2}$ | $R_{3}$ | $R_{4}$ | $R_{5}$
---|---|---|---|---|---
$t_{1}$ | N | - | - | - | N
$t_{2}$ | W | E | - | W | E
$t_{3}$ | S | - | - | - | S
$...$ | $...$ | $...$ | $...$ | $...$ | $...$

Table 1: Each table displays the three first observables at times $t_{1}$,
$t_{2}$, and $t_{3}$ for three TESs in the behavior of the product of
components $R_{1}$, $R_{2}$, $R_{3}$, $R_{4}$, and $R_{5}$ on the grid of
Figure 1. We omit the subscript and use the column to identify the events. The
symbol - represents the absence of observation in the TES.

We write the composite cyber-physical system consisting of $5$ robot
components interacting with a shared grid as the following expression:

$R_{1}\bowtie R_{2}\bowtie R_{3}\bowtie R_{4}\bowtie R_{5}\bowtie
G(\\{1,2,3,4,5\\},5,2)$

Three first observations for three behaviors are displayed in Table 1. Each
behavior exposes different degrees of concurrency, where in the left behavior,
only robot $R_{1}$ moves, while in the middle behavior, robots $R_{1}$ and
$R_{2}$ swap their positions, and in the right behavior both $R_{1}$ and
$R_{4}$ swap their positions with $R_{2}$ and $R_{5}$, respectively.

###  2.3 Properties of components and coordination

A component $C=(E,L)$ may satisfy some properties on its behavior. We consider
trace properties $P\subseteq\mathit{TES}(E)$ and say that $C$ satisfies $P$ if
and only if $L\subseteq P$, i.e., all the behavior of $C$ is included in the
property $P$.

For the set of robots and the grid, we consider the following property:
_eventually, the position of each robot $R_{i}$ is $(i,0)_{R_{i}}$_, i.e.,
every robot successfully reaches its place.

This property is a trace property, which we call $P_{\mathit{sorted}}$ and
consists of every behavior $\sigma\in\mathit{TES}(E)$ such that there exists
an $n\in\mathbb{N}$ with $\sigma(n)=(O_{n},t_{n})$ and $(i,0)_{R_{i}}\in
O_{n}$ for all robots $R_{i}$. As shown in Table 1, the set of behaviors for
the product of robots is large, and the property $P_{\mathit{sorted}}$ does
not (necessarily) hold _a priori_ : there exists a composite behavior $\tau$
for the component $R_{1}\bowtie R_{2}\bowtie R_{3}\bowtie R_{4}\bowtie
R_{5}\bowtie G(\\{1,2,3,4,5\\},5,2)$ such that $\tau\not\in
P_{\mathit{sorted}}$.

Robots may beforehand decide on some strategies to swap and move on the grid
such that their composition satisfies the property $P_{\mathit{sorted}}$. For
instance, consider the following strategy for each robot $R_{n}$:

  * •

_swapping_ : if the last read $(x,y)$ of its location is such that $x<n$, then
move North, then West, then South.

  * •

_pursuing_ : otherwise, move East.

Remember that the grid prevents two robots from moving to the same cell, which
is therefore removed from the observable behavior. We emphasize that some
sequences of moves for each robot may deadlock, and therefore are not part of
the behavior of the system of robots. Consider Figure 2, for which each robot
follows its internal strategy. Because of non-determinism introduced by the
timing of each observations, one may consider the following sequence of
observations: first, $R_{1}$ move North, then West; in the meantime, $R_{2}$
moves West, followed by $R_{3}$, $R_{4}$, and $R_{5}$. By a similar sequence
of moves, the set of robots ends in the configuration on the right of Figure
2. In this position and for each robot, the next move dictated by its internal
strategy is disallowed, which corresponds to a _deadlock_. While behaviors do
not contain finite sequences of observations, which makes the scenario of
Figure 2 not expressible as a TES, such scenario may occur in practice. We
give in next Section some analysis to prevent such behavior to happen.

$R_{5}$$R_{4}$$R_{3}$$R_{2}$$R_{1}$

$\Rightarrow$

$R_{1}$$R_{5}$$R_{4}$$R_{3}$$R_{2}$

$\Rightarrow$

$R_{3}$$R_{2}$$R_{4}$$R_{5}$$R_{1}$

Figure 2: Initial state of the unsorted robot (left) leading to a possible
deadlock (right) if each robot follows its strategy.

Alternatively, the collection of robots may be coordinated by an external
protocol that guides their moves. Besides considering the robot and the grid
components, we add a third kind of component that acts as a coordinator. In
other words, we make the protocol used by robots to interact explicit and
external to them and the grid; i.e., we assume exogenous coordination.
Exogenous coordination allows robots to decide a priori on some strategies to
swap and move on the grid, in which case their external coordinator component
merely unconditionally facilitates their interactions. Alternatively, the
external coordinator component may implement a protocol that guides the moves
of a set of clueless robots into their destined final locations. The most
intuitive of such coordinator is the property itself as a component. Indeed,
let $C_{\mathit{sorted}}=(E,L)$ be such that $E=\bigcup_{i\in I}E_{R_{i}}$
with $I=\\{1,2,3,4,5\\}$ and $L=P_{\mathit{sorted}}$. Then, and as shown in
[9], the coordinated component $R_{1}\bowtie R_{2}\bowtie R_{3}\bowtie
R_{4}\bowtie R_{5}\bowtie G(\\{1,2,3,4,5\\},5,2)\bowtie C_{\mathit{sorted}}$
trivially satisfies the property $P_{\mathit{sorted}}$. While easily
specified, such coordination component is non-deterministic and not easily
implementable. We provide an example of a deterministic coordinators.

Given two robot identifiers $R_{1}$ and $R_{2}$, we introduce the swap
component $S(R_{1},R_{2})$ that coordinates the two robots $R_{1}$ and $R_{2}$
to swap their positions. Its interface $E_{S}(R_{1},R_{2})$ contains the
following events:

  * •

start(S($R_{1}$,$R_{2}$)) and end(S($R_{1}$, $R_{2}$)) that respectively
notify the beginning and the end of an interaction with $R_{1}$ and $R_{2}$.
Those events are observed when the swap protocol is starting or ending an
interaction with either $R_{1}$ or with $R_{2}$.

  * •

$(x,y)_{R_{1}}$ and $(x,y)_{R_{2}}$ that occur when the protocol reads,
respectively, the position of robot $R_{1}$ and robot $R_{2}$,

  * •

$d_{R_{1}}$ and $d_{R_{2}}$ for all $d\in\\{N,W,E,S\\}$ that occur when the
robots $R_{1}$ and $R_{2}$ move;

  * •

locked(S($R_{1}$,$R_{2}$)) and unlocked(S($R_{1}$,$R_{2}$)) that occur,
respectively, when another protocol begin and end an interaction with either
$R_{1}$ and $R_{2}$.

The behavior of a swapping protocol $S(R_{1},R_{2})$ is such that, it starts
its protocol sequence by an observable start(S($R_{1},R_{2}$)), then it moves
$R_{1}$ North, then $R_{2}$ East, then $R_{1}$ West and South. The protocol
starts the sequence only if it reads a position for $R_{1}$ and $R_{2}$ such
that $R_{1}$ is on the cell next to $R_{2}$ on the $x$-axis. Once the sequence
of moves is complete, the protocol outputs the observable end(S($R_{1}$,
$R_{2}$)). If the protocol is not swapping two robots, or is not locked, then
robots can freely read their positions.

Swapping protocols interact with each others by locking other protocols that
share the same robot identifiers. Therefore, if S($R_{1}$,$R_{2}$) starts its
protocol sequence, then S($R_{2}$, $R_{i}$) synchronizes with a locked event
locked(S($R_{2}$,$R_{i}$)), for $2<i$. Then, $R_{2}$ cannot swap with other
robots unless S($R_{1}$,$R_{2}$) completes its sequence, in which case
end(S($R_{1}$, $R_{2}$)) synchronizes with unlocked(S($R_{2}$,$R_{i}$)) for
$2<i$. We extend the underlying composability relation $\sqcap$ on observables
such that, for all $(O_{1},O_{2})\in\sqcap$ and $i<j$:

$\displaystyle\text{start(S($R_{i}$,$R_{j}$))}\in O_{1}\implies$
$\displaystyle\exists k.k<i.\text{locked(S($R_{k}$, $R_{i}$))}\in O_{2}\lor$
$\displaystyle\exists k.j<k.\text{locked(S($R_{j}$, $R_{k}$))}\in O_{2}$

and

$\displaystyle\text{end(S($R_{i}$,$R_{j}$))}\in O_{1}\implies$
$\displaystyle\exists k<i.\text{unlocked(S($R_{k}$, $R_{i}$))}\in O_{2}\lor$
$\displaystyle\exists j<k.\text{unlocked(S($R_{j}$, $R_{k}$))}\in O_{2}$

For each pair of robots $R_{i}$, $R_{j}$ such that $i<j$, we introduce a
swapping protocol S($R_{i}$, $R_{j}$). As a result, the coordinated system is
given by the following composition:

$R_{1}\bowtie R_{2}\bowtie R_{3}\bowtie R_{4}\bowtie R_{5}\bowtie
G(\\{1,2,3,4,5\\},5,2)\bowtie_{i<j}S(R_{i},R_{j})$

Note that the definition of $\sqcap$ and of $\kappa_{\sqcap}^{\mathit{sync}}$
impose that, if one protocol starts its sequence, then all protocols that
share some robot identifiers synchronize with a lock event. Similar behavior
occurs at the end of the sequence.

The study of the coordinated system, and the analysis of its possible deadlock
is the object of Section 3. We give an operational specification of components
using TES transition systems. We define the possibility for such operational
components to deadlock, and give some conditions to prevent deadlock from
occurring given a composition of deadlock free components.

##  3 An operational specification of components

In Section 2.1, we give a declarative specification of components, and
considers infinite behaviors only. We give, in Section 3.1, an operational
specification of components using TES transition systems. We relate the
parametrized product of TES transition systems with the parametrized product
on their corresponding components, and show its correctness. The composition
of two TES transition systems may lead to transitions that are not composable,
and ultimately to a deadlock, i.e., a state with no outgoing transitions.

###  3.1 TES transition systems.

The behavior of a component as in Definition 1 is a set of TESs. We give an
operational definition of such set using a labelled transition system.

######  Definition 3 (TES transition system)

A TES transition system is a triple $(Q,E,\rightarrow)$ where $Q$ is a set of
states, $E$ is a set of events, and $\rightarrow\subseteq
Q\times(\mathcal{P}(E)\times\mathbb{R}_{+})\times Q$ is a labeled transition
relation, where labels are observations. $\triangle$

We present two different ways to give a semantics to a TES transition system:
inductive and co-inductive. Both definitions give the same behavior, as shown
in Theorem 3.1, and we use interchangeably each definition to simplify the
proofs of, e.g., Theorem 3.2.

#### Semantics 1 (runs).

Let $T=(Q,E,\rightarrow)$ be a TES transition system. Given
$s\in(\mathcal{P}(E)\times\mathbb{R}_{+})^{n}$, we write $q\xrightarrow{s}p$
for the sequence of transitions
$q\xrightarrow{s(0)}q_{1}\xrightarrow{s(1)}q_{2}\ ...\xrightarrow{s(n)}p$. We
use $\to^{*}$ and $\to^{\omega}$ to denote, respectively, the set of finite
and infinite sequences of consecutive transitions in $\to$. Then, finite
sequences of observables form the set
$\mathcal{L}^{\mathrm{fin}}(T,q)=\\{\sigma\in\mathit{TES}(E)\mid
q\xrightarrow{s}q^{\prime},\exists
n.s=\sigma[n]\land\sigma^{(n)}\in\mathit{TES}(\emptyset)\\}$ and infinite
ones, the set
$\mathcal{L}^{\mathrm{inf}}(T,q)=\\{\sigma\in\mathit{TES}(E)\mid\forall
n.\sigma[n]\in\mathcal{L}^{\mathrm{fin}}(T,q)\\}$ where, as introduced above,
$\sigma[n]$ is the prefix of size $n$ of $\sigma$. The semantics of such a TES
transition system $T=(Q,E,\rightarrow)$, starting in a state $q\in Q$, is the
component $C_{T}(q)=(E,\mathcal{L}^{\mathrm{inf}}(T,q))$.

#### Semantics 2 (greatest post fixed point)

Alternatively, the semantics of a TES transition system is the greatest post
fixed point of a function over sets of TESs paired with a state. For a TES
transition system $T=(Q,E,\to)$, let
$\mathcal{R}\subseteq\mathit{TES}(E)\times Q$. We introduce
$\phi_{T}:\mathcal{P}(\mathit{TES}(E)\times
Q)\rightarrow\mathcal{P}(\mathit{TES}(E)\times Q)$ as the function:

$\begin{array}[]{rl}\phi_{T}(\mathcal{R})=\\{(\tau,q)\mid&\exists p\in Q,\
q\xrightarrow{\tau(0)}p\land(\tau^{\prime},p)\in\mathcal{R}\\}\end{array}$

We can show that $\phi_{T}$ is monotonous, and therefore $\phi_{T}$ has a
greatest post fixed point
$\Omega_{T}=\bigcup\\{\mathcal{R}\mid\mathcal{R}\subseteq\phi_{T}(\mathcal{R})\\}$.
We write $\Omega_{T}(q)=\\{\tau\mid(\tau,q)\in\Omega_{T}\\}$ for any $q\in Q$.
Note that the two semantics coincide.

######  Theorem 3.1 (Equivalence)

For all $q\in Q$,
$\mathcal{L}^{\mathrm{inf}}(T,q)=\\{\tau\mid(\tau,q)\in\Omega_{T}\\}$.

###### Proof

Let $T=(Q,E\to)$ and $\Omega_{T}(q)=\\{\tau\mid(\tau,q)\in\Omega_{T}\\}$.

$\begin{array}[]{rl}\tau\in\Omega_{T}(c_{0})\iff&(\tau,c_{0})\in\Omega_{T}\\\
\iff&c_{0}\xrightarrow{\tau(0)}c_{1}\land(\tau^{\prime},c_{1})\in\Omega_{T}\\\
\iff&\exists\chi\in\rightarrow^{\omega}.\
\chi(0)=c_{0}\xrightarrow{\tau(0)}c_{1}\land(\tau^{\prime},c_{1})\in\Omega_{T}\\\
\iff&\exists\chi\in\rightarrow^{\omega},c\in Q^{\omega}.\ c(0)\in
Q_{0}\land\forall n\in\mathbb{N}.\\\
&\chi(n)=c(n)\xrightarrow{\tau(n)}c(n+1)\land(\tau^{(n+1)},c(n+1))\in\Omega_{T}\\\
\iff&\exists\chi\in\to^{\omega}.\
\chi(0)=c_{0}\xrightarrow{\tau(0)}c_{1}\land\tau\in\mathcal{L}^{\mathrm{inf}}(T,q)\\\
\iff&\tau\in\mathcal{L}^{\mathrm{inf}}(T,q)\end{array}$

In the fourth equivalence, we state that the infinite sequence
$\chi\in\rightarrow^{\omega}$ has, as sequence of labels, the sequence of
observations in $\tau$. We prove the step by induction. Let $n\in\mathbb{N}$,
and let $\chi\in\rightarrow^{\omega}$ be such that, for all $k\leq n$,
$\chi(k)=c_{k}\xrightarrow{\tau(k)}c_{k+1}$ with $c_{k}\in Q$ and
$(\tau^{(k)},c_{k})\in\Omega_{T}$. Then, given that
$(\tau^{(n)},c_{n})\in\Omega_{T}$, there exists a transition
$c_{n}\xrightarrow{\tau(n+1)}c_{n+1}$ and there exists $\rho\in\to^{\omega}$
such that, for all $k\leq n$, $\rho=\chi$ and
$r(n+1)=c_{n}\xrightarrow{\tau(n+1)}c_{n+1}$, which proves the implication.
The other direction of the equivalence is simpler. If there exists
$\chi\in\to^{\omega}$ such that for all $n\in\mathbb{N}$,
$\chi(n)=c_{n}\xrightarrow{\tau(n)}c_{n+1}$, then we have a witness, for every
$n\in\mathbb{N}$, that $(\tau^{(n)},c_{n})$ is an element of $\Omega_{T}$. ∎

######  Remark 1 (Deadlock)

Observe that
$\mathit{FG}(\mathcal{L}^{\mathrm{inf}}(T,q))\subseteq\mathcal{L}^{\mathrm{fin}}(T,q)$
which, in the case of strict inclusion, captures the fact that some states may
have no outgoing transitions and therefore deadlock.

######  Remark 2 (Expressivness)

There may be two different TES transition systems $T_{1}$ and $T_{2}$ such
that $\mathcal{L}^{\mathrm{inf}}(T_{1})=\mathcal{L}^{\mathrm{inf}}(T_{2})$,
i.e., a set of TESs is not uniquely characterized by a TES transition system.

###### Example 1

The behavior of a robot introduced earlier is a TES transition system
$T_{R}=(\mathbb{R}_{+},E_{R},\rightarrow)$ where
$t\xrightarrow{(\\{e\\},t)}t+\delta$ for abitrary $t$ and $\delta$ in
$\mathbb{R}_{+}$ and $e\in E_{R}$.

Similarly, the behavior of a grid is a TES transition system
$T_{G}(I,n,m)=(Q_{G},E_{G}(I,n,m),\rightarrow)$ where:

  * •

$Q_{G}\subseteq\mathbb{R}_{+}\times(I\to([0;n]\times[0;m]))$,

  * •

$(t,f)\xrightarrow{(O,t)}(t+\delta,f^{\prime})$ for abitrary $t$ and $\delta$
in $\mathbb{R}_{+}$, such that

    * –

$d_{R}\in O$ implies $f^{\prime}(R)$ is updated according to the direction $d$
if the resulting position is within the bounds of the grid;

    * –

$(x,y)_{R}\in O$ implies $f(R)=(x,y)_{R}$ and $f^{\prime}(R)=f(R)$;

    * –

$f^{\prime}(R)=f(R)$, otherwise.

The behavior of a swap protocol S($R_{i}$,$R_{j}$) with $i<j$ is a TES
transition system $T_{S}(R_{1},R_{2})=(Q,E,\to)$ where, for
$t_{1},t_{2},t_{3},t_{4}\in\mathbb{R}_{+}$ with $t_{1}<t_{2}<t_{3}<t_{4}$:

  * •

$Q\subseteq\mathbb{R}_{+}\times\\{s_{1},s_{2},s_{3},s_{4},s_{6}\\}$;

  * •

$E=E_{R_{i}}\cup
E_{R_{j}}\cup\\{\mathit{lock}(R_{i},R_{j}),\mathit{unlock}(R_{i},R_{j}),\mathit{start}(R_{i},R_{j}),\mathit{end}(R_{i},R_{j})\\}$

  * •

$(t_{1},s_{1})\xrightarrow{(\\{\mathit{lock}(R_{i},R_{j})\\},t_{1})}(t_{2},s_{2})$;

  * •

$(t_{1},s_{2})\xrightarrow{(\\{\mathit{unlock}(R_{i},R_{j})\\},t_{1})}(t_{2},s_{1})$;

  * •

$(t_{1},s_{1})\xrightarrow{(\\{\mathit{start}(R_{i},R_{j}),(x,y)_{R_{i}},(x+1,y)_{R_{j}}\\},t_{1})}(t_{2},s_{3})$;

  * •

$(t_{1},s_{3})\xrightarrow{(\\{N_{R_{j}}\\},t_{1})}(t_{2},s_{4})\xrightarrow{(\\{\\{W_{R_{j}},E_{R_{i}}\\}\\},t_{2})}(t_{3},s_{5})\xrightarrow{(\\{\\{S_{R_{j}}\\}\\},t_{3})}(t_{4},s_{6})$;

  * •

$(t_{1},s_{6})\xrightarrow{(\\{\mathit{end}(R_{i},R_{j})\\},t_{1})}(t_{2},s_{1})$;

$\blacksquare$

The product of two components is parametrized by a composability relation and
a composition function and syntactically constructs the product of two TES
transition systems.

######  Definition 4 (Product)

The product of two TES transition systems $T_{1}=(Q_{1},E_{1},\to_{1})$ and
$T_{2}=(Q_{2},E_{2},\to_{2})$ under the constraint $\kappa$ is the TES
transition system $T_{1}\times_{\kappa}T_{2}=(Q_{1}\times Q_{2},E_{1}\cup
E_{2},\to)$ such that:

$\cfrac{q_{1}\xrightarrow{(O_{1},t_{1})}_{1}q_{1}^{\prime}\quad
q_{2}\xrightarrow{(O_{2},t_{2})}_{2}q_{2}^{\prime}\quad((O_{1},t_{1}),(O_{2},t_{2}))\in\kappa(E_{1},E_{2})\quad
t_{1}<t_{2}}{(q_{1},q_{2})\xrightarrow{(O_{1},t_{1})}(q_{1}^{\prime},q_{2})}$
$\cfrac{q_{1}\xrightarrow{(O_{1},t_{1})}_{1}q_{1}^{\prime}\quad
q_{2}\xrightarrow{(O_{2},t_{2})}_{2}q_{2}^{\prime}\quad((O_{1},t_{1}),(O_{2},t_{2}))\in\kappa(E_{1},E_{2})\quad
t_{2}<t_{1}}{(q_{1},q_{2})\xrightarrow{(O_{2},t_{2})}(q_{1},q_{2}^{\prime})}$
$\cfrac{q_{1}\xrightarrow{(O_{1},t_{1})}_{1}q_{1}^{\prime}\quad
q_{2}\xrightarrow{(O_{2},t_{2})}_{2}q_{2}^{\prime}\quad((O_{1},t_{1}),(O_{2},t_{2}))\in\kappa(E_{1},E_{2})\quad
t_{1}=t_{2}}{(q_{1},q_{2})\xrightarrow{(O_{1}\cup
O_{2},t_{1})}(q_{1}^{\prime},q_{2}^{\prime})}$

$\triangle$

Observe that the product is defined on pairs of transitions, which implies
that if $T_{1}$ or $T_{2}$ has a state without outgoing transition, then the
product has no outgoing transitions from that state. The reciprocal is,
however, not true in general.

Theorem 3.2 states that the product of TES transition systems denotes (given a
state) the set of TESs that corresponds to the product of the corresponding
components (in their respective states). Then, the product that we define on
TES transition systems does not add nor remove behaviors with respect to the
product on their respective components.

######  Theorem 3.2 (Correctness)

For all TES transition systems $T_{1}$ and $T_{2}$, and for all composability
relation $\kappa$:

$C_{T_{1}\times_{\kappa}T_{2}}(q_{1},q_{2})=C_{T_{1}}(q_{1})\times_{([\kappa],[\cup])}C_{T_{2}}(q_{2})$

###### Proof

Let $T_{1}=(Q_{1},E_{1},\to_{1})$ and $T_{2}=(Q_{2},E_{2},\to_{2})$. The proof
goes in two directions:

  1. 1.

We first show that, for any $\tau$ in the behavior of
$\mathcal{L}^{\mathrm{inf}}(T_{1}\times_{\kappa}T_{2},(q_{1},q_{2}))$, there
exist $\tau_{1}\in\mathcal{L}^{\mathrm{inf}}(T_{1},q_{1})$ and
$\tau_{2}\in\mathcal{L}^{\mathrm{inf}}(T_{2},q_{2})$ such that
$\tau=\tau_{1}[\cup]\tau_{2}$ and
$(\tau_{1},\tau_{2})\in[\kappa](E_{1},E_{2})$.

  2. 2.

We then show that, for any
$\tau_{1}\in\mathcal{L}^{\mathrm{inf}}(T_{1},q_{1})$ and
$\tau_{2}\in\mathcal{L}^{\mathrm{inf}}(T_{2},q_{2})$ such that
$(\tau_{1},\tau_{2})\in[\kappa](E_{1},E_{2})$, we have
$(\tau_{1}[\cup]\tau_{2})\in\mathcal{L}^{\mathrm{inf}}(T_{1}\times_{\kappa}T_{2},(q_{1},q_{2}))$.

We recall the definition of
$\Phi_{\kappa}:\mathcal{P}(\mathit{TES}(E)\times\mathit{TES}(E))\rightarrow\mathcal{P}(\mathit{TES}(E)\times\mathit{TES}(E))$,
the function defining the lifting of $\kappa$ from observations to TESs (by
co-induction), to be such that, for all
$\mathcal{R}\subseteq\mathit{TES}(E)\times\mathit{TES}(E)$:

$\begin{array}[]{rl}\Phi_{\kappa}(\mathcal{R})=\\{(\tau_{1},\tau_{2})\mid&\tau_{1}(0)=(O_{1},t_{1})\land\tau_{2}(0)=(O_{2},t_{2})\
\land\\\
&(\tau_{1}(0),\tau_{2}(0))\in\kappa(E_{1},E_{2})\land[t_{1}<t_{2}\land(\tau_{1}^{\prime},\tau_{2})\in\mathcal{R}\lor\\\
&\hskip 120.00018pt\
t_{2}<t_{1}\land(\tau_{1},\tau_{2}^{\prime})\in\mathcal{R}\lor\\\ &\hskip
120.00018pt\
t_{1}=t_{2}\land(\tau_{1}^{\prime},\tau_{2}^{\prime})\in\mathcal{R}]\\}\end{array}$

First, observe that, by construction, for all
$\tau\in\Omega_{T_{1}\times_{\kappa}T_{2}}(q_{1},q_{2})$, there exist
$\tau_{1}\in\Omega_{T_{1}}(q_{1})$ and $\tau_{2}\in\Omega_{T_{2}}(q_{2})$ such
that $\tau=\tau_{1}[\cup]\tau_{2}$. Indeed, each transition in
$T_{1}\times_{\kappa}T_{2}$ is constructed out of a composable pair of
observations from a transition in $T_{1}$ and in $T_{2}$. The resulting label
is identical to the label that $[\cup]$ defines co-inductively. Moreover, each
element $\tau\in\Omega_{T_{1}\times_{\kappa}T_{2}}(q_{1},q_{2})$ contains
infinitely many labels from $T_{1}$ and from $T_{2}$, due to the assumption
that a TES has an increasing an non-Zeno sequence of time stamps.

We therefore use $\widetilde{\Omega}_{T_{1}\times_{\kappa}T_{2}}(q_{1},q_{2})$
to denote the set of such pairs. We then prove that, for all $(q_{1},q_{2})\in
Q_{1}\times Q_{2}$,
$(\tau_{1},\tau_{2})\in\widetilde{\Omega}_{T_{1}\times_{\kappa}T_{2}}(q_{1},q_{2})$
implies that $(\tau_{1},\tau_{2})\in[\kappa](E_{1},E_{2})$ and
$(\tau_{1},\tau_{2})\in\Omega_{T_{1}}(q_{1})\times\Omega_{T_{2}}(q_{2})$.

We prove that
$\widetilde{\Omega}_{T_{1}\times_{\kappa}T_{2}}(q_{1},q_{2})=\\{(\tau_{1},\tau_{2})\in[\kappa](E_{1},E_{2})\mid(\tau_{1},\tau_{2})\in\Omega_{T_{1}}(q_{1})\times\Omega_{T_{2}}(q_{2})\\}$
by showing forward and backward inclusion, i.e., point $1$ and point $2$
respectively.

Forward inclusion. We know that since
$(\tau_{1},\tau_{2})\in\widetilde{\Omega}_{T_{1}\times_{\kappa}T_{2}}(q_{1},q_{2})$,
then there exists a post fixed point $R$ of $\Phi_{T_{1}\times_{\kappa}T_{2}}$
such that $((\tau_{1},\tau_{2}),(q_{1},q_{2}))\in R$. Let $\widetilde{R}$ be
the set $\\{(\tau_{1},\tau_{2})\mid\exists q.((\tau_{1},\tau_{2}),q)\in R\\}$.
We show that $\widetilde{R}$ is a post fixed point of $[\kappa](E_{1},E_{2})$.
By definition of the transition relation $\to$ of $T_{1}\times_{\kappa}T_{2}$,
we have that if $(\tau_{1},\tau_{2})\in\widetilde{R}$, then
$(\tau_{1}(0),\tau_{2}(0))\in\kappa(E_{1},E_{2})$ and, if $t_{1}<t_{2}$ then
$(\tau_{1}^{\prime},\tau_{2})\in\widetilde{R}$, if $t_{2}<t_{1}$ then
$(\tau_{1},\tau_{2}^{\prime})\in\widetilde{R}$, and if $t_{1}=t_{2}$ then
$(\tau_{1}^{\prime},\tau_{2}^{\prime})\in\widetilde{R}$. We thus conclude that
$\widetilde{R}\subseteq\Phi_{\kappa}(\widetilde{R})$, and therefore
$\widetilde{\Omega}_{T_{1}\times_{\kappa}T_{2}}(q_{1},q_{2})\subseteq[\kappa](E_{1},E_{2})$.

We then showed that, for any $\tau$ in the behavior of
$\mathcal{L}^{\mathrm{inf}}(T_{1}\times_{\kappa}T_{2},(q_{1},q_{2}))$, there
exist $\tau_{1}\in\mathcal{L}^{\mathrm{inf}}(T_{1},q_{1})$ and
$\tau_{2}\in\mathcal{L}^{\mathrm{inf}}(T_{2},q_{2})$ such that
$\tau=\tau_{1}[\cup]\tau_{2}$ and
$(\tau_{1},\tau_{2})\in[\kappa](E_{1},E_{2})$.

Backward inclusion. We show that, for all $(q_{1},q_{2})\in Q_{1}\times
Q_{2}$, if $(\tau_{1},\tau_{2})\in[\kappa](E_{1},E_{2})$ and
$(\tau_{1},\tau_{2})\in\Omega_{T_{1}}(q_{1})\times\Omega_{T_{2}}(q_{2})$ then
$(\tau_{1},\tau_{2})\in\widetilde{\Omega}_{T_{1}\times_{\kappa}T_{2}}(q_{1},q_{2})$.

To do so, we construct a post fixed points of $\Phi_{\kappa}$, which we denote
$S$, such that $((\tau_{1},\tau_{2}),(q_{1},q_{2}))\in S$; and, for all
$((\tau,\sigma),(q,s))\in S$, we have $\tau(0)=(O_{1},t_{1})$ and
$\sigma(0)=(O_{2},t_{2})$:

  * •

if $t_{1}<t_{2}$ and
$(q_{1},q_{2})\xrightarrow{\tau(0)}(q_{1}^{\prime},q_{2})$ then
$((\tau^{\prime},\sigma),(q_{1}^{\prime},q_{2}))\in S$;

  * •

if $t_{2}<t_{1}$ and
$(q_{1},q_{2})\xrightarrow{\sigma(0)}(q_{1},q_{2}^{\prime})$ then
$((\tau,\sigma^{\prime}),(q_{1},q_{2}^{\prime}))\in S$; and

  * •

if $t_{2}=t_{1}$ and
$(q_{1},q_{2})\xrightarrow{\sigma(0)\cup\tau(0)}(q_{1}^{\prime},q_{2}^{\prime})$
then $((\tau^{\prime},\sigma^{\prime}),(q_{1}^{\prime},q_{2}^{\prime}))\in S$.

Since $(\tau_{1},\tau_{2})\in[\kappa](E_{1},E_{2})$, we know that
$S\subseteq[\kappa](E_{1},E_{2})$. We now show that
$S\subseteq\Phi_{T_{1}\times_{\kappa}T_{2}}(S)$. The argument for $S$ being a
post fixed point of $\Phi_{T_{1}\times_{\kappa}T_{2}}$ follows from the
definition of $S$.

∎

We give in Example 2 the TES transition systems resulting from the product of
the TES transition systems of two robots and a grid. Example 2 defines
operationally the components in Section 2.2, i.e., their behavior is generated
by a TES transition system.

###### Example 2

Let $T_{R_{1}}$, $T_{R_{2}}$ be two TES transition systems for robots $R_{1}$
and $R_{2}$, and let $T_{G}(\\{1\\},n,m)$ be a grid with robot $R_{1}$ alone
and $T_{G}(\\{1,2\\},n,m)$ be a grid with robots $R_{1}$ and $R_{2}$. Let
$E=E_{1}\cup E_{2}\cup E_{G}$ and
$\sqcap\subseteq\mathcal{P}(E)\times\mathcal{P}(E)$ be such that
$(O_{1},O_{2})\in\sqcap$ if and only if $O_{1}=O_{2}\subseteq E_{R}\cap
E_{G}$. We use $\kappa_{\sqcap}^{\mathit{sync}}$ as defined in [9].

The product of $T_{R_{1}}$, $T_{R_{2}}$, and $T_{G}(\\{1,2\\},n,m)$ under
$\kappa_{\sqcap}^{\mathit{sync}}$ is the TES transition system
$T_{R_{1}}\times_{\kappa_{\sqcap}^{\mathit{sync}}}T_{R_{2}}\times_{\kappa_{\sqcap}^{\mathit{sync}}}T_{G}(\\{1,2\\},n,m)$
such that it synchronizes observations of the two robots with the grid, but
does not synchronize events of the two robots directly, since the two set of
events are disjoint.

$\blacksquare$

As a consequence of Theorem 1, letting $\kappa_{\sqcap}^{\mathit{sync}}$ be
the composability relation used in the product $\bowtie$ and writing
$T=T_{R_{1}}\times_{\kappa_{\sqcap}^{\mathit{sync}}}T_{R_{2}}\times_{\kappa_{\sqcap}^{\mathit{sync}}}T_{G}$,
$C_{T}(q1,q2,q3)$ is equal to the component $C_{T_{R_{1}}}(q_{1})\bowtie
C_{T_{R_{2}}}(q_{2})\bowtie C_{T_{G}}(q_{3})$

Let $T$ be a TES transition system, and let
$C_{T}(q)=(E,\mathcal{L}^{\mathrm{inf}}(T,q))$ be a component whose behavior
is defined by $T$. Then, $C$ is _deadlock free_ if and only if
$\mathit{FG}(\mathcal{L}^{\mathrm{inf}}(T,q))=\mathcal{L}^{\mathrm{fin}}(T,q)$.

A class of deadlock free components is that of components that accept
arbitrary insertion of $\emptyset$ observables in between two observations. We
say that such component is _prefix-closed_ , as every sequence of finite
observations can be continued by an infinite sequence of empty observables,
i.e., $C$ is such that $C=C^{*}$ (as defined after Definition 2). We say that
a TES transition system $T$ is prefix-closed if and only if and only if
$C_{T}(q)=C^{*}_{T}(q)$. For instance, if $T$ is such that, for any state $q$
and for any $t\in\mathbb{R}_{+}$ there is a transition
$q\xrightarrow{(\emptyset,t)}q$, then $T$ is prefix-closed.

###### Lemma 1

If $T_{1}$ and $T_{2}$ are prefix-closed, then
$T_{1}\times_{\kappa_{\sqcap}^{\mathit{sync}}}T_{2}$ is prefix-closed where
$\sqcap\subseteq\mathcal{P}(E_{1})\times\mathcal{P}(E_{2})$ with
$(O_{1},O_{2})\in\sqcap$ implies $O_{1}\not=\emptyset$ and
$O_{2}\not=\emptyset$.

###### Proof

The proof follows from the fact that $\emptyset$ is independent with any non-
empty observable $O\subseteq E_{1}\cup E_{2}$. Then, any pair of silent
observation is composable, and therefore the following TES transition system
is prefix-closed. ∎

We search for the condition under which deadlock freedom is preserved under a
product. Section 3.3 gives a condition for the product of two deadlock free
components to be deadlock free.

###  3.2 Compatibility of components

Informally, the condition of $\kappa$-compatibility from two TES transition
systems $T_{1}$ and $T_{2}$ translates the existence of a relation
$\mathcal{R}$ on pairs of states of $T_{1}$ and $T_{2}$ such that
$(q_{1},q_{2})\in\mathcal{R}$ and for every state $(q,s)\in\mathcal{R}$, every
outgoing transition from $T_{1}$ (reciprocally $T_{2}$) has a transition in
$T_{2}$ that composes under $\kappa$. In all cases, the pair of outgoing
states is in the relation $\mathcal{R}$.

Formally, a TES transition system $T_{1}=(Q_{1},E_{1},\to_{1})$ from state
$q_{1}$ is $\kappa$-compatible with a TES transition system
$T_{2}=(Q_{2},E_{2},\to_{2})$ from state $q_{2}$, and we say $(T_{1},q_{1})$
is $\kappa$-compatible with $(T_{2},q_{2})$, if there exists a relation
$\mathcal{R}\subseteq Q_{1}\times Q_{2}$ such that,
$(q_{1},q_{2})\in\mathcal{R}$ and for any $(p_{1},p_{2})\in\mathcal{R}$,

  * •

there exist $p_{1}\xrightarrow{(O_{1},t_{1})}_{1}r_{1}$ and
$p_{2}\xrightarrow{(O_{2},t_{2})}_{2}r_{2}$ such that
$((O_{1},t_{1}),(O_{2},t_{2}))\in\kappa(E_{1},E_{2})$; and

  * •

for all $p_{1}\xrightarrow{(O_{1},t_{1})}_{1}r_{1}$ and
$p_{2}\xrightarrow{(O_{2},t_{2})}_{2}r_{2}$ if
$((O_{1},t_{1}),(O_{2},t_{2}))\in\kappa(E_{1},E_{2})$ then
$(u_{1},u_{2})\in\mathcal{R}$, where $u_{i}=r_{i}$ if
$t_{i}=\min\\{t_{1},t_{2}\\}$, and $u_{i}=p_{i}$ otherwise for
$i\in\\{1,2\\}$.

In other words, if $(T_{1},q_{1})$ is $\kappa$-compatible with
$(T_{2},q_{2})$, then all transitions in $T_{1}$ starting in $q_{1}$
eventually match some composable transitions in $T_{2}$ starting in $q_{2}$.
If $(T_{2},q_{2})$ is $\kappa$-compatible to $(T_{1},q_{1})$ as well, then we
say that $(T_{1},q_{1})$ and $(T_{2},q_{2})$ are $\kappa$-compatible.

######  Theorem 3.3 (Deadlock free)

Let $(T_{1},q_{1})$ and $(T_{2},q_{2})$ be $\kappa$-compatible. Let
$C_{T_{1}}(q_{1})$ and $C_{T_{2}}(q_{2})$ be deadlock free. Then,
$C_{T_{1}}(q_{1})\times_{([\kappa],[\cup])}C_{T_{2}}(q_{2})$ is deadlock free.

###### Proof

We reason by contradiction. If the product
$C_{T_{1}}(q_{1})\times_{([\kappa],[\cup])}C_{T_{2}}(q_{2})$ is not deadlock
free, then
$\mathcal{L}^{\mathrm{fin}}(T_{1}\times_{\kappa}T_{2},(q_{1},q_{2}))\not=\mathit{FG}(\mathcal{L}^{\mathrm{inf}}(T_{1}\times_{\kappa}T_{2},(q_{1},q_{2})))$.
Thus, there exists a state $(s,q)$, reachable from $(q_{1},q_{2})$, such that
$\mathcal{L}^{\mathrm{fin}}(T_{1}\times_{\kappa}T_{2},(s,q))=\emptyset$. Given
the fact that both TES transition systems are deadlock free, and given that
$s$ (respectively $q$) is reachable from $q_{1}$ (respectively $q_{2}$) for
$T_{1}$ (respectively $T_{2}$), then
$\mathcal{L}^{\mathrm{fin}}(T_{2},q_{1})\not=\emptyset$ and
$\mathcal{L}^{\mathrm{fin}}(T_{1},q_{2})\not=\emptyset$.

Since $(T_{1},q_{1})$ and $(T_{2},q_{2})$ are $\kappa$-compatible, then there
exists $\mathcal{R}$ such that for each pair $(s,q)\in\mathcal{R}$, there
exists an outgoing transition in $T_{1}$ and $T_{2}$ from $s$ and $q$
respectively that is composable under $\kappa$. Such property would imply that
there is a transition in $T_{1}\times_{\kappa}T_{2}$ from state $(s,q)$ and
therefore
$\mathcal{L}^{\mathrm{fin}}(T_{1}\times_{\kappa}T_{2},(s,q))\not=\emptyset$.
In other words, the property of compatibility contradicts the presence of
deadlock in the product
$C_{T_{1}}(q_{1})\times_{([\kappa],[\cup])}C_{T_{2}}(q_{2})$. ∎

###### Lemma 2

If $T_{1}=(Q_{1},E_{1},\rightarrow_{1})$ and
$T_{2}=(Q_{1},E_{1},\rightarrow_{1})$ are deadlock free and are such that
$\sqcap\cap(\mathcal{P}(E_{1})\times\mathcal{P}(E_{2}))=\emptyset$, then
$(T_{1},q_{1})$ is $\kappa_{\sqcap}^{\mathit{sync}}$-compatible with
$(T_{2},q_{2})$ for arbitrary $(q_{1},q_{2})\in Q_{1}\times Q_{2}$.

###### Proof

If the relation $\sqcap$ does not relate any observables, then any pair of
observations is composable under $\kappa^{\mathit{sync}}_{\sqcap}$. As a
consequence, any sequence of transitions is allowed. ∎

###### Lemma 3

If $T_{1}$ and $T_{2}$ are prefix-closed, then $(T_{1},q_{1})$ and
$(T_{2},q_{2})$ are $\kappa^{\mathit{sync}}_{\sqcap}$-compatible for arbitrary
$q_{1}\in Q_{1}$, $q_{2}\in Q_{2}$, and
$\sqcap\subseteq\mathcal{P}(E_{1})\times\mathcal{P}(E_{2})$ with
$(O_{1},O_{2})\in\sqcap$ implies $O_{1}\not=\emptyset$ and
$O_{2}\not=\emptyset$.

###### Proof

Follows from Lemma 1.

The consequence of two TES transition systems $T_{1}$ and $T_{2}$ to be
$\kappa$-compatible on $(q_{1},q_{2})$ and deadlock free, is that they can be
run _step-by-step_ from $(q_{1},q_{2})$ (i.e., the product can be done at
runtime), and the resulting behavior is an element of
$\mathcal{L}^{\mathrm{inf}}(T_{1}\times_{\kappa}T_{2},(q_{1},q_{2}))$. In
general however, $\kappa$-compatibility is not preserved over product,
demonstrated by Example 3. For the case of coordinated cyber-physical systems,
components are usually not prefix-closed as there might be some timing
constraints or some mandatory actions to perform in a bounded time frame.

###### Example 3

Suppose three TES transition systems
$T_{i}=(\\{q_{i}\\},\\{a,b,c,d\\},\to_{i})$, with $i\in\\{1,2,3\\}$, defined
as follow for all $n\in\mathbb{N}$:

  * •

$q_{1}\xrightarrow{(\\{a,b\\},n)}_{1}q_{1}$ and
$q_{1}\xrightarrow{(\\{a,c\\},n)}_{1}q_{1}$;

  * •

$q_{2}\xrightarrow{(\\{a,c\\},n)}_{2}q_{2}$ and
$q_{2}\xrightarrow{(\\{a,d\\},n)}_{2}q_{2}$;

  * •

$q_{3}\xrightarrow{(\\{a,d\\},n)}_{3}q_{3}$ and
$q_{3}\xrightarrow{(\\{a,b\\},n)}_{3}q_{3}$.

Let $\sqcap=\\{(O,O)\mid O\subseteq\\{a,b,c,d\\}\\}$. It is easy to show that
$T_{1}(q_{1})$, $T_{2}(q_{2})$, and $T_{3}(q_{3})$ are pairwise
$\kappa^{\mathit{sync}}_{\sqcap}$-compatible. However, $T_{1}(q_{1})$ is not
$\kappa^{\mathit{sync}}_{\sqcap}$-compatible with
$T_{2}(q_{2})\times_{\sqcap}^{\mathit{sync}}T_{3}(q_{3})$.

$\blacksquare$

Note that, if $(T_{1},q_{1})$, $(T_{2},q_{2})$, and $(T_{3},q_{3})$ are
pairwise $\kappa$-compatible TES transition systems, and if one of the
following holds:

  * •

$T_{1}$, $T_{2}$, $T_{3}$ are all three prefix-closed TES transition systems;

  * •

$\sqcap\cap(\mathcal{P}(E_{1})\times\mathcal{P}(E_{2})\cup\mathcal{P}(E_{2})\times\mathcal{P}(E_{3})\cup\mathcal{P}(E_{1})\times\mathcal{P}(E_{3}))=\emptyset$;
or

  * •

$T_{1}$, $T_{2}$, $T_{3}$ are such that, for all of their state, there is one
and only one outgoing transition.

then $(T_{1},q_{1})$ and $(T_{2}\times_{\kappa}T_{3},(q_{2},q_{3}))$ are
pairwise $\kappa^{\mathit{sync}}_{\sqcap}$-compatible.

##  4 Application: self-sorting robots

We implemented in Maude a framework to simulate concurrent executions of TES
transition systems, where time stamps are restricted to natural numbers. Using
the description given in Example 1 for the grid and for robots, we add to
their composition several protocols that aim at preventing deadlock. The
source for the implementation is accessible at [1] to reproduce the results of
this section.

#### Components in Maude

The implementation of TES transition systems in Maude focuses on a subset that
has some properties. First, TES transition systems in Maude have time stamps
that range over the set of positive natural numbers $\mathbb{N}$. We do not
implement components with real time.

Second, TES transition systems are delay insensitive. This property encodes
that arbitrary time may pass for each transition in the TES transition system.
Then, a TES transition system that is delay insensitive is such that if
$q\xrightarrow{(O,n)}p$, then $q\xrightarrow{(O,n+k)}p$ for arbitrary
$k\in\mathbb{N}$. We therefore write $q\xrightarrow{O}p$ to denote the set of
transitions $q\xrightarrow{(O,n)}p$ for all $n\in\mathbb{N}$.

In Maude, the state of a TES transition system component is represented by a
term and the state of a composed system is a multiset of component states.
Transitions of the step-wise product are defined in terms of such system
states. For instance, the swap protocol between robot $R(3)$ and $R(1)$ is the
following term in Maude:

⬇

[swap(R(3),R(1)): Protocol | k("state") |-> ds(q(0)); false; null]

where swap(R(3),R(1)) is the name of the component; Protocol is its class;
k(“state”) maps to the initial state of the protocol q(0); “false” denotes the
status of the protocol; and “null” is the set of transitions that the protocol
may take.

#### Runtime composition.

The product of TES transition systems is constructed at runtime, step by step.
We fix a composability relation $\kappa_{\sqcap}^{\mathit{sync}}$ to be such
that, for all $O\subseteq\mathbb{E}$, $(O,O)\in\sqcap$. We use
$\kappa_{\sqcap}^{\mathit{sync}}$ for the product of TES transition systems.

Given a list of initialized TES transition system, the runtime computes the
set of all possible composite transitions, from which transitions that violate
the composability relation $\kappa_{\sqcap}^{\mathit{sync}}$ are filtered out,
and one transition that is composable is non-deterministically chosen.

Algorithm 1 Runtime composition

1:

2:\- $n$ initialized TES transition systems
$S=\\{T_{1}(q_{1}),...,T_{n}(q_{n})\\}$

3:\- composability relation $\sqcap$ over observables

4:procedure RuntimeComposition

5: for $T_{i}(q_{i})\in S$ do

6: add $\\{q_{i}\xrightarrow{O_{i}}_{i}p_{i}\mid p_{i}\in Q_{i}\\}$ to Tr

7: while $trs_{i},trs_{j}\in\textit{Tr}$ do

8: for $q_{i}\xrightarrow{O_{i}}p_{i}\in trs_{i}$ and
$q_{j}\xrightarrow{O_{j}}p_{j}\in trs_{j}$ do

9: if $((O_{i},1),(O_{j},2))\in\kappa^{\mathit{sync}}_{\sqcap}(E_{i},E_{j})$
then

10: add $(q_{i},q_{j})\xrightarrow{O_{i}}(p_{i},q_{j})$ to $\textit{trs}_{ij}$

11: if $((O_{i},2),(O_{j},1))\in\kappa^{\mathit{sync}}_{\sqcap}(E_{i},E_{j})$
then

12: add $(q_{i},q_{j})\xrightarrow{O_{j}}(q_{i},p_{j})$ to $\textit{trs}_{ij}$

13: if $((O_{i},1),(O_{j},1))\in\kappa^{\mathit{sync}}_{\sqcap}(E_{i},E_{j})$
then

14: add $(q_{i},q_{j})\xrightarrow{O_{i}\cup O_{j}}(p_{i},p_{j})$ to
$\textit{trs}_{ij}$

15:
$\textit{Tr}:=(\textit{Tr}\setminus\\{\textit{trs}_{i},\textit{trs}_{i}\\})\cup\\{\textit{trs}_{ij}\\}$

16: let $trs\in\textit{Tr}$

17: let $(q_{1},...,q_{n})\xrightarrow{O}(r_{1},....,r_{n})\in trs$

18: for $i\leq n$ do

19: $T_{i}(q_{i})\Rightarrow T_{i}(r_{i})$

Algorithm 1 shows the procedure RuntimeComposition that corresponds to a one
step product of the input TES transition systems. Note that such procedure
applied recursively on its results would generate a behavior that is in
behavior of the product of the TES transition systems.

#### Results.

Initially, the system consists of three _trolls_ , with identifiers
$\mathit{id(0)}$, $\mathit{id(1)}$, and $\mathit{id(2)}$, each coordinated by
two protocols $\mathit{swap(id(i),id(j))}$ with $i,j\in\\{0,1,2\\}$ and $j<i$.
The trolls move on a grid and trolls $\mathit{id(0)}$, $\mathit{id(1)}$, and
$\mathit{id(2)}$ are respectively initialized at position $(2;0)$, $(1;0)$,
and $(0;0)$. 111We refer to [4] for a more detailed description of the Maude
framework. The property $P_{\mathit{sorted}}$ is a reachability property on
the state of the grid, that states that _eventually, all robots are in the
sorted position_. In Maude, we express such reachability property with the
following search command:

⬇

search [1] init =>*

[sys::Sys [ field : Field | k((0;0)) |-> d(id(0)),

k((1;0)) |-> d(id(1)),

k((2;0)) |-> d(id(2)) ; true ; null]] .

Table 2 features three variations on the sorting problem. The first system is
composed of robots whose move are free on the grid. The second adds one
battery for each component, whose energy level decreases for each robot move.
The third system adds a swap protocol for every pair of two robots. The last
system adds protocol and batteries to compose with the robots.

We record, for each of those systems, whether the sorted configuration is
reachable ($P_{\mathit{sorted}}$), and if all three robots can run out of
energy ($P_{\mathit{battery-out}}$).

Table 2: Evaluation of different systems for several behavioral properties. System | $P_{\mathit{sorted}}$ | $P_{b}$
---|---|---
$\underset{0\leq i<2}{\bowtie}R_{i}\bowtie G$ |  $12.10^{3}$ states, 25s, $31.10^{6}$ rewrites | -
$\underset{0\leq i<2}{\bowtie}(R_{i}\bowtie B_{i})\bowtie G$ |  $12.10^{3}$ states, 25s, $31.10^{6}$ rewrites | true
$\underset{0\leq i<2}{\bowtie}R_{i}\bowtie G\underset{0\leq i<j<2}{\bowtie}S(R_{i},R_{j})$ |  $8250$ states, 44s, $80.10^{6}$ rewrites | -
$\underset{0\leq i<2}{\bowtie}(R_{i}\bowtie B_{i})\bowtie G\underset{0\leq i<j<2}{\bowtie}S(R_{i},R_{j})$ |  $8250$ states, 71s, $83.10^{6}$ rewrites | false

Observe that the reachability query returns a solution for both system: the
one with and without protocols. However, the time to reach the first solution
increases as the number of states and transition increases (adding the
protocol components). We leave as future work some optimization to improve on
our results.

##  5 Related work

#### Discrete Event Systems

Our work represents both cyber and physical aspects of system with a unified
model of discrete event systems. In [8], the author lists the current
challenges in modelling cyber-physical in such a way. The author points to the
problem of modular control, where even though two modules run without problems
in isolation, the same two modules may block when they are used in
conjunction.

In [11], the authors present procedures to synthesize supervisors that control
a set of interacting processes and, in the case of failure, report a
diagnosis. Cyber-physical systems have also been studied from an actor-model
perspective, where actors interact through events [12, 6]. In our work, we add
to the event structure a timing constraint, and expose condition to take the
product of discrete event systems at runtime.

#### Synchronization of processes

In [10], the author describes infinite behaviors of process and their
synchronization. Notably, the problem of non-blockingness is stated: if two
processes eventually interact on some actions, how to make sure that both
processes will not block each others. The concept of centrality of a process
is introduced, which corresponds to our definition of deadlock freedom. Our
work extends this work in that it gives sufficient conditions to compute at
runtime, using a step-wise product, some behaviors in the synchronous product.

#### Components

In [2], the authors give a co-inductive definition of components, to which [9]
is an extension. In [3], the authors propose a state based specification as
constraint automata. A transition in a constraint automata is labeled by a
guarded command, whose satisfaction depends on the context of its product
(other constraint automata). Except from [7], constraint automata do not have
time as part of their semantics (i.e., only specify time insensitive
components), and only describe observables on ports. In that respect, our
model extends constraint automata by generalizing the set of possible
observables, and adding the time of the observable as part of the transition.

#### Timed systems

In [5], the authors use heterogeneous timed asynchronous relational nets (HT-
ARNs) to model timed sensitive components, and a specification as timed IO-
automata. The authors show some conditions (progress-enabledness and
r-closure) for the product of two HT-ARNs to preserve progress-enabledness. We
may have recover a similar result, but with some modifications. Our product is
more expressive: $\kappa$ needs not be only synchronization of shared events,
but can have more intricate coordination [9] (e.g., exclusion of two events).
We do not necessitate our process to be $r$-closed, and in general, we do not
want to explicitly write the silent observations.

##  6 Conclusion

We introduced an operational specification of cyber-physical components
introduced in [9], for which we gave sufficient conditions for some products
to be correctly implemented at runtime. As a consequence, we implemented our
framework in Maude, and use our correctness result to show that our analysis
are sound. We finally proved an emergent sorting property our of a set of
robots whose moves on a grid are coordinated by a local swapping protocol.

#### Acknowledgement

Talcott was partially supported by the U. S. Office of Naval Research under
award numbers N00014-15-1-2202 and N00014-20-1-2644, and NRL grant
N0017317-1-G002. Arbab was partially supported by the U. S. Office of Naval
Research under award number N00014-20-1-2644.

## References

  * [1] , https://scm.cwi.nl/FM/cp-agent
  * [2] Farhad Arbab and Jan Rutten  “A Coinductive Calculus of Component Connectors”, 2002, pp. 34–55  DOI: 10.1007/978-3-540-40020-2˙2
  * [3] Christel Baier, Marjan Sirjani, Farhad Arbab and Jan Rutten  “Modeling component connectors in Reo by constraint automata” Second International Workshop on Foundations of Coordination Languages and Software Architectures (FOCLASA’03)  In _Science of Computer Programming_ 61.2, 2006, pp. 75–113  DOI: https://doi.org/10.1016/j.scico.2005.10.008
  * [4] Manuel Clavel et al.  “All About Maude: A High-Performance Logical Framework” 4350, LNCS  Springer, 2007
  * [5] José Luiz Fiadeiro and Antónia Lopes  “Heterogeneous and asynchronous networks of timed systems”  In _Theor. Comput. Sci._ 663, 2017, pp. 1–33  DOI: 10.1016/j.tcs.2016.12.014
  * [6] Tobias Kappé, Benjamin Lion, Farhad Arbab and Carolyn L. Talcott  “Soft component automata: Composition, compilation, logic, and verification”  In _Sci. Comput. Program._ 183, 2019  DOI: 10.1016/j.scico.2019.08.001
  * [7] Natallia Kokash, Mohammad Mahdi Jaghoori and Farhad Arbab  “From Timed Reo Networks to Networks of Timed Automata” Proceedings the 9th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA)  In _Electronic Notes in Theoretical Computer Science_ 295, 2013, pp. 11–29  DOI: https://doi.org/10.1016/j.entcs.2013.04.004
  * [8] Stéphane Lafortune  “Discrete Event Systems: Modeling, Observation, and Control”  In _Annual Review of Control, Robotics, and Autonomous Systems_ 2.1, 2019, pp. 141–159  DOI: 10.1146/annurev-control-053018-023659
  * [9] Benjamin Lion, Farhad Arbab and Carolyn L. Talcott  “A Semantic Model for Interacting Cyber-Physical Systems”  In _Proceedings 14th Interaction and Concurrency Experience, ICE 2021, Online, 18th June 2021_ 347, EPTCS, 2021, pp. 77–95  DOI: 10.4204/EPTCS.347.5
  * [10] Maurice Nivat  “Behaviors of Processes and Synchronized Systems of Processes”  In _Theoretical Foundations of Programming Methodology: Lecture Notes of an International Summer School, directed by F. L. Bauer, E. W. Dijkstra and C. A. R. Hoare_ Dordrecht: Springer Netherlands, 1982, pp. 473–551  DOI: 10.1007/978-94-009-7893-5˙14
  * [11] Meera Sampath, Stéphane Lafortune and Demosthenis Teneketzis  “Active diagnosis of discrete-event systems”  In _IEEE Trans. Autom. Control._ 43.7, 1998, pp. 908–929  DOI: 10.1109/9.701089
  * [12] Carolyn Talcott  “Cyber-Physical Systems and Events”  In _Software-Intensive Systems and New Computing Paradigms: Challenges and Visions_ Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 101–115  DOI: 10.1007/978-3-540-89437-7˙6

##  7 Appendix

We recall a list of results for showing algebraic properties of product on
components given properties of composability relation on observables.

###### Property 1

We list a series of properties on a composability relation on observable
$\sqcap$ where, for $O_{1},O_{2},O_{3}\subseteq\mathbb{E}$:

  1. 1.

if $\mathit{ind}_{\sqcap}(O_{1},O_{2})$ and
$\mathit{ind}_{\sqcap}(O_{1},O_{3})$ then
$\mathit{ind}_{\sqcap}(O_{1},O_{2}\cup O_{3})$; and if
$\mathit{ind}_{\sqcap}(O_{2},O_{3})$ and $\mathit{ind}_{\sqcap}(O_{1},O_{3})$
then $\mathit{ind}_{\sqcap}(O_{1}\cup O_{2},O_{3})$

  2. 2.

if $(O_{1},O_{2})\in\sqcap$ and $(O_{2},O_{3})\in\sqcap$, then
$(O_{1},O_{3})\in\sqcap$;

  3. 3.

if $(O_{1},O_{2})\in\sqcap$ and $(O_{1},O_{3})\in\sqcap$, then
$(O_{2},O_{3})\in\sqcap$ and $(O_{3},O_{2})\in\sqcap$;

  4. 4.

if $(O_{1},O_{3})\in\sqcap$ and $(O_{2},O_{3})\in\sqcap$, then
$(O_{1},O_{2})\in\sqcap$ and $(O_{2},O_{1})\in\sqcap$;

  5. 5.

if $(O_{1},O_{2})\in\sqcap$ and $(O_{1}^{\prime},O_{2}^{\prime})\in\sqcap$,
then $(O_{1}\cup O_{1}^{\prime},O_{2}\cup O_{2}^{\prime})\in\sqcap$.

###### Corollary 1

Let $\sqcap$ be a composability relation on observables and
$\kappa^{\mathit{sync}}_{\sqcap}$ the synchronous composability relation on
observations. Then:

  * •

if $\sqcap$ is symmetric, then the product
$\times_{([\kappa^{\mathit{sync}}_{\sqcap}],[\cup])}$ is commutative;

  * •

if $\sqcap$ satisfies Properties 1, then the product
$\times_{([\kappa^{\mathit{sync}}_{\sqcap}],[\cup])}$ is associative;

  * •

if $\sqcap$ is co-reflexive, i.e., $(O_{1},O_{2})\in\sqcap$ implies
$O_{1}=O_{2}$, then the product
$\times_{([\kappa^{\mathit{sync}}_{\sqcap}],[\cup])}$ is idempotent.