University of Oxford, UK<EMAIL_ADDRESS>https://orcid.org/0000-0001-6899-9971 Imperial College London,
<EMAIL_ADDRESS>https://orcid.org/0000-0002-6431-4100
University of Oxford<EMAIL_ADDRESS>https://orcid.org/0000-0002-3925-8557 <ccs2012> <concept>
<concept_id>10011007.10010940.10011003.10011687</concept_id>
<concept_desc>Software and its engineering Software usability</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10011007.10011006.10011008.10011009.10011014</concept_id>
<concept_desc>Software and its engineering Concurrent programming
languages</concept_desc> <concept_significance>500</concept_significance>
</concept> <concept>
<concept_id>10003752.10003753.10003761.10003764</concept_id>
<concept_desc>Theory of computation Process calculi</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Software and its engineering Software usability [500]Software and its
engineering Concurrent programming languages [500]Theory of computation
Process calculi MnLargeSymbols’164 MnLargeSymbols’171

# Fearless Asynchronous Communications with Timed Multiparty Session Protocols

Ping Hou Nicolas Lagaillardie Nobuko Yoshida

###### Abstract

Session types using  _affinity_ and  _exception handling_ mechanisms have been
developed to ensure the communication safety of protocols implemented in
concurrent and distributed programming languages. Nevertheless, current affine
session types are inadequate for specifying real-world asynchronous protocols,
as they are usually imposed by _time constraints_ which enable _timeout
exceptions_ to prevent indefinite blocking while awaiting valid messages. This
paper proposes the first formal integration of  _affinity_ , _time
constraints_ , _timeouts_ , and  _time-failure handling_ based on multiparty
session types for supporting reliability in asynchronous distributed systems.
With this theory, we statically guarantee that asynchronous timed
communication is deadlock-free, communication safe, while being _fearless_ –
never hindered by timeout errors or abrupt terminations.

To implement our theory, we introduce $\texttt{MultiCrusty}^{T}$, a Rust
toolchain designed to facilitate the implementation of safe affine timed
protocols. $\texttt{MultiCrusty}^{T}$ leverages generic types and the time
library to handle timed communications, integrated with optional types for
affinity. We evaluate our approach by extending diverse examples from the
literature to incorporate time and timeouts, demonstrating that our solution
incurs negligible overhead compared with an untimed implementation. We also
showcase the  _correctness by construction_ of our approach by implementing
various real-world use cases, including a remote data protocol from the
Internet of Remote Things domain, as well as protocols from real-time systems
like Android motion sensors and smartwatches.

###### keywords:

Session Types, Concurrency, Time Failure Handling, Affinity, Timeout, Rust

##  1 Introduction

#### Background

The growing prevalence of distributed programming has emphasised the
significance of prioritising  _reliability_ in distributed systems. Dedicated
research efforts focus on enhancing reliability through the study and
modelling of failures. This research enables the design of more resilient
distributed systems, capable of effectively handling failures and ensuring
reliable operation.

A lightweight, type-based methodology, which ensures basic reliability –
_safety_ in distributed communication systems, is _session types_ [20]. This
type discipline is further advanced by _Multiparty Session Types_ (MPST) [21,
22], which enable the specification and verification of communication
protocols among multiple message-passing processes in concurrent and
distributed systems. MPST ensure that protocols are designed to prevent common
safety errors, i.e. deadlocks and communication mismatches during interactions
among many participants [21, 22, 43]. By adhering to a specified MPST
protocol, participants (a.k.a. end-point programs) can communicate reliably
and efficiently. From a practical perspective, MPST have been implemented in
various programming languages [7, 30, 32, 36, 47, 50], facilitating their
applications and providing safety guarantees in real-world programs.

Nevertheless, tackling the challenges of unreliability and failures remains a
significant issue for session types. Most session type systems operate under
the assumption of flawless and reliable communication without failures. To
address this limitation, recent works [35, 18, 19, 32] have developed  _affine
session types_ by incorporating the  _affinity_ mechanism that explicitly
accounts for and handles unreliability and failures within session type
systems. Unlike linear types that must be used _exactly_ once, affine types
can be used _at most_ once, enabling the safe dropping of subsequent types and
the premature termination of a session in the presence of protocol execution
errors.

In most real-life devices and platforms, communications are predominantly
asynchronous: inner tasks and message transfers may take time. When dealing
with such communications, it becomes crucial to incorporate  _time
constraints_ and implement  _timeout failure handling_ for each operation.
This is necessary to avoid potential blockages where a process might wait
indefinitely for a message from a non-failed process. While various works, as
explained later, address time conditions and timeouts in session types, it is
surprising that none of the aforementioned works on affine session types
tackles the handling of timeout failures during protocol execution.

#### This Paper

introduces a new framework, _affine timed multiparty session types_ (ATMP), to
address the challenges of timeouts, disconnections and other failures in
asynchronous communications:  (1) We propose ATMP, an extension of
asynchronous MPST that incorporates time specifications, affinity, and
mechanisms for handling exceptions, thus facilitating effective management of
failures, with a particular focus on timeouts. Additionally, we demonstrate
that properties from MPST, i.e.  _type safety_ , _protocol conformance_ , and
_deadlock-freedom_ , are guaranteed for well-typed processes, even in the
presence of timeouts and their corresponding handling mechanism;  (2) We
present $\texttt{MultiCrusty}^{T}$, our Rust toolchain designed for building
asynchronous timed multiparty protocols under ATMP:
$\texttt{MultiCrusty}^{T}$ enables the implementation of protocols adhering
to the properties of ATMP.

The primary focus of ATMP lies in effectively  _handling_ timeouts during
process execution, in contrast to the approaches in [6, 5], which aim to
completely _avoid_ time failures. Bocchi et al. [6] introduce time conditions
in MPST to ensure precise timing in communication protocols, while their
subsequent work [5] extends _binary_ timed session types to incorporate
timeouts, allowing for more robust handling of time constraints. Yet, they
adopt strict requirements to  _prevent_ timeouts. In [6], _feasibility_ and
_wait-freedom_ are required in their protocol design. Feasibility requires
precise time specifications for protocol termination, while wait-freedom
prohibits overlapping time windows for senders and receivers in a protocol,
which is not practical in real-world applications. Similarly, in [5], strong
conditions including  _progress_ of an entire set of processes and  _urgent
receive_ are imposed. The progress property is usually _undecidable_ , and the
urgent receive condition, which demands immediate message reception upon
availability, is infeasible with asynchronous communication.

Recently, [34] proposes the inclusion of timeout as the unique failure
notation in MPST, offering flexibility in handling failures. Time also plays a
role in _synchronous_ communication systems, where [25] develops _rate_ -based
_binary_ session types, ensuring _synchronous_ message exchanges at the same
_rate_ , i.e. within the same time window. However, in both [34] and [25],
time constraints are not integrated into types and static type checking,
resulting in the specifications lacking the ability to guide time behaviour.
Additionally, the model used in [25] assumes that all communications and
computations are non-time-consuming, i.e. with zero time cost, making it
unfeasible in distributed systems.

By the efficient integration of time and failure handling mechanisms in our
framework, none of those impractical requirements outlined in [6, 5] is
necessary. In ATMP, when a process encounters a timeout error, a mechanism for
handling time failures is triggered, notifying all participants about the
timeout, leading to the termination of those participants and ultimately
ending the session. Such an approach guarantees that participants consistently
reach the  _end of the protocol_ , as the communication session is entirely
dropped upon encountering a timeout error. As a result, every process can
terminate successfully, reducing the risk of indefinite blockages, even with
timeouts. Additionally, in our system, time constraints over local clocks are
incorporated with types to effectively model asynchronous timed communication,
addressing the limitations in [34, 25].

Except for [25], the aforementioned works on timed session types focus more on
theory, lacking implementations. To bridge this gap on the practical side, we
provide $\texttt{MultiCrusty}^{T}$, a Rust implementation of ATMP designed
for secure timed communications. $\texttt{MultiCrusty}^{T}$ makes use of
affine timed meshed channels, a communication data structure that integrates
time constraints and clock utilisation. Our toolchain relies on macros and
native generic types to ensure that asynchronous protocols are inherently
_correct by construction_. In particular, $\texttt{MultiCrusty}^{T}$ performs
compile-time verification to guarantee that, at any given point in the
protocol, each isolated pair of participants comprises one sender and one
receiver with corresponding time constraints. Additionally, we employ affine
asynchronous primitives and native optional types to effectively handle
_runtime_ timeouts and errors.

To showcase the capabilities and expressiveness of our toolchain, we evaluate
$\texttt{MultiCrusty}^{T}$ through examples from the literature, and further
case studies including a remote data protocol from an Internet of Remote
Things (IoRT) network [9], a servo web protocol from a web engine [44], and
protocols from real-time systems such as Android motion sensor [2], PineTime
smartwatch [39], and keyless entry [48]. Our comparative analysis with a Rust
implementation of affine MPST without time [32] reveals that
$\texttt{MultiCrusty}^{T}$ exhibits minimal overhead while providing
significantly strengthened property checks.

#### Contributions and Structure

§ 2 offers a comprehensive overview of our theory and toolchain, employing
the  _remote data_ as a running example. § 3 provides a session
$\pi$-calculus for ATMP that incorporates timeout, affinity, asynchrony, and
failure handling mechanisms. § 4 introduces an extended theory of
asynchronous multiparty session types with time annotations, elucidating the
behavioural correspondence between timed types in Thms. 4.10 and 4.9.
Additionally, we present a typing system for ATMP session $\pi$-calculus, and
demonstrate the properties of typed processes, including subject reduction
(processes preserve well-typedness), session fidelity (processes adhere to
their types), and deadlock-freedom (processes never get stuck), in Thms. 4.16,
4.21 and 4.24. § 5 delves into the design and usage of
$\texttt{MultiCrusty}^{T}$, our Rust implementation of ATMP. § 6 showcases
the compilation and execution benchmarks of $\texttt{MultiCrusty}^{T}$, based
on selected case studies. Finally, § 7 concludes the paper by discussing
related work, and offering conclusions and potential future work. Full proofs,
auxiliary material, and more details of $\texttt{MultiCrusty}^{T}$ can be
found in Appendix. Additionally, our toolchain and evaluation examples are
available in an artifact, which can be accessed on Zenodo. For those
interested in the source files, they are available on GitHub.

##  2 Overview

In this section, we give an overview of affine timed multiparty session types
(ATMP) and $\texttt{MultiCrusty}^{T}$, our toolchain for implementing affine
timed asynchronous protocols. First, we share a real-world example inspiring
our work on affine asynchronous timed communication.

Fig. 1(b) depicts our running example, _remote data_. This real-world scenario
is sourced from a satellite-enabled Internet of Remote Things network [9], and
describes data transmissions among a _Sensor_
($\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sen}}}$),
a _Server_
($\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$),
and a _Satellite_
($\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$):
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
aims to periodically retrieve data gathered by
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sen}}}$
via
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$.
The protocol revolves around a loop initiated by
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$,
which faces a decision: either retrieve data or end the protocol. In the
former scenario,
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
requests data retrieval from
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sen}}}$
with a message labelled _GetData_ via
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
within the time window of 5 and 6 time units, as indicated by clock
constraints (i.e. $5\leq
C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}\leq
6$, where
$C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}$
is the clock associated with
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$).
Upon receiving this request,
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sen}}}$
responds by sending the data with a message labelled _Data_ to
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
through
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
within 6 and 7 time units, followed by clock resets denoted as reset
predicates (i.e.
$C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}:=0$,
resetting the clock to 0). In the alternative branch,
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
sends a _Close_ message to
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$,
which is then forwarded to
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sen}}}$,
between 5 and 6 time units.

Our remote data protocol includes internal tasks that consume time, notably
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sen}}}$
requiring 5 time units to gather data before transmitting. In cases where our
protocol lacks a specified timing strategy (i.e. no time requirements), and
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sen}}}$
cannot accomplish the data-gathering tasks, it results in indefinite blocking
for
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
and
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
as they await the data. This could lead to undesirable outcomes, including
partially processed data, data corruption, or incomplete transmission of
processed data. Therefore, incorporating time constraints into communication
protocols is imperative, as it better reflects real-world scenarios and
ensures practical viability.

###  2.1 ATMP: Theory Overview

Section 4Section 3Section 5Thms 4.16, 4.21, 4.24 Type CheckingSection
4Processes withAffinity, Time, and TimeoutsTimed Local TypesTimed Global
Type$\nu$ScrTCommunicatingTimed Automata$\texttt{MultiCrusty}^{T}$Programs
writtenwith $\texttt{MultiCrusty}^{T}$
APIProjectionGenerationTypeCheckingProjectionThms 4.9, 4.10 (a) Top-down view
of ATMP (left) and $\texttt{MultiCrusty}^{T}$ (right).

(b) Global protocol for _remote data_.

Figure 1: Overview of affine asynchronous communication with time.

Our ATMP theory follows the _top-down_ methodology [21, 22], enhancing
asynchronous MPST with time features to facilitate timed global and local
types. As shown in Fig. 1(a) (left), we specify multiparty protocols with time
as  _timed global types_. These timed global types are projected into  _timed
local types_ , which are then used for type-checking processes with affine
types, time, timeouts, and failure handling, written in a session calculus. As
an example, we consider a simple communication scenario derived from remote
data: the Satellite
($\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$)
communicates with the server
($\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$)
by sending a  _Data_ message
(${\color[rgb]{0.43,0.21,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.43,0.21,0.1}\mathtt{Data}}$).
Specifically,
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
needs to send the message between 6 and 7 time units and reset its clock
afterwards, while
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
is expected to receive the message within the same time window and reset its
clock accordingly.

#### Timed Types and Processes

This communication behaviour can be represented by the timed global type
${\color[rgb]{0.43,0.21,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.43,0.21,0.1}G}$:

$\small{\color[rgb]{0.43,0.21,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.43,0.21,0.1}{\color[rgb]{0.43,0.21,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.43,0.21,0.1}{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}{\to}{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}{:}\left\\{{{\color[rgb]{0.43,0.21,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.43,0.21,0.1}{\color[rgb]{0.43,0.21,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.43,0.21,0.1}\mathtt{Data}}\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}6\leq
C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}\leq
7,C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}:=0,6\leq
C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}\leq
7,C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}:=0}\\}\vphantom{x}\\!\mathbin{{\color[rgb]{0.43,0.21,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.43,0.21,0.1}.}}\\!{{\color[rgb]{0.43,0.21,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.43,0.21,0.1}\mathbf{end}}}}}\right\\}}}$

where
$C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}$
and
$C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}$
denote the clocks of
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
and
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$,
respectively. A global type represents a protocol specification involving
multiple roles from a global standpoint.

Adhering to the MPST top-down approach, a timed global type is then
_projected_ onto timed local types, which describe communications from the
perspective of individual roles. In our example,
${\color[rgb]{0.43,0.21,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.43,0.21,0.1}G}$
is projected onto two timed local types, one for each role
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
and
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$:

$\small{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}T_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}=\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\oplus}{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\mathtt{Data}}{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}6\leq
C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}\leq
7,C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}:=0}\\}}\mathbin{\\!{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}.}\\!}{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\mathbf{end}}\quad{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}T_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}=\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\&}{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\mathtt{Data}}{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}6\leq
C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}\leq
7,C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}:=0}\\}}\mathbin{\\!{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}.}\\!}{\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\mathbf{end}}$

Here
${\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}T_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}$
indicates that
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
sends
(${\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\oplus}$)
the message
${\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\mathtt{Data}}$
to
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
between 6 and 7 time units and then immediately resets its clock
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}$.
Dually,
${\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}T_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}$
denotes
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
receiving
(${\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}\&}$)
the message from
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
within the same time frame and resetting its clock
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}C_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}$.

In the final step of the top-down approach, we employ timed local types to
conduct type-checking for processes, denoted as
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}$, in
the ATMP session calculus. Our session calculus extends the framework for
_affine multiparty session types_ (AMPST) [32] by incorporating processes that
model time, timeouts, and asynchrony. In our example,
${\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}T_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}$
and
${\color[rgb]{0,0,0.9}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.9}T_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}$
are used for the type-checking of
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}]}$
and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}]}$,
which respectively represent the channels (a.k.a. session endpoints) played by
roles
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
and
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
in a multiparty session
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}$, within
the processes:

$\small{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({C_{1}=6.5})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}]}}^{0.4}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}}]\mathbin{\\!\oplus\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{Data}}}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbf{0}}}}}}}\quad{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}={\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({C_{2}=6})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}]}}^{0.3}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}}]{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{Data}}}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbf{0}}}}}}}$

The Satellite process
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}$
waits for exactly 6.5 time units
(${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}(C_{1}=6.5)}$),
then sends the message
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{Data}}$
with a timeout of 0.4 time units
(${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}]}}^{0.4}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}}]\mathbin{\\!\oplus\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{Data}}}}}}$),
and becomes inactive
(${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbf{0}}$).
Meanwhile, the Server process
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}$
waits for 6 time units
(${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}(C_{2}=6)}$),
then receives the message with a timeout of 0.3 time units
(${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}]}}^{0.3}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}}]{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{Data}}}}}}$),
subsequently becoming inactive.

#### Solution to Stuck Processes Due to Time Failures

It appears that the parallel execution of
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}$
and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}$,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}}$,
cannot proceed further due to the disparity in timing requirements.
Specifically, using the same session
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}$,
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
sends the message
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{Data}}$
to
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
between 6.5 and 6.9 time units, while
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
must receive it from
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
between 6 and 6.3 time units. This results in a stuck situation, as
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
cannot meet the required timing condition to receive the message.

Fortunately, in our system, timeout failures are allowed, which can be
addressed by leveraging affine session types and their associated failure
handling mechanisms. Back to our example, when
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}]}$
waits for 6 time units and cannot receive
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{Data}}$
within 0.3 time units, a timeout failure is raised
(${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}]}}^{0.3}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}}}}]{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{Data}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbf{0}}}}}]$).
Furthermore, we apply our time-failure handling approach to manage this
timeout failure, initiating the termination of the channel
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}}]}$
and triggering the cancellation process of the session
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}$
(${{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$).
As a result, the process will successfully terminate by canceling (or killing)
all usages of
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}$ within
it.

Conversely, the system introduced in [6] enforces strict requirements,
including  _feasibility_ and  _wait-freedom_ , on timed global types to
prevent time-related failures in well-typed processes, thus preventing them
from becoming blocked due to unsolvable timing constraints. Feasibility
ensures the successful termination of each allowed partial execution, while
wait-freedom guarantees that receivers do not have to wait if senders follow
their time constraints. In our example, we start with a timed global type that
is neither feasible nor wait-free, showcasing how our system effectively
handles time failures and ensures successful process termination without
imposing additional conditions on timed global types. In essence, reliance on
feasibility and wait-freedom becomes unnecessary in our system, thanks to the
inclusion of affinity and time-failure handling mechanisms.

###  2.2 $\texttt{MultiCrusty}^{T}$: Toolchain Overview

⬇ 1struct Send<T, 2 const CLOCK: char, 3 const START: i128, 4 const
INCLUDE_START: bool, 5 const END: i128, 6 const INCLUDE_END: bool, 7 const
RESET: char, 8 S>
---
(a) Send type

⬇ 1struct Recv<T, 2 const CLOCK: char, 3 const START: i128, 4 const
INCLUDE_START: bool, 5 const END: i128, 6 const INCLUDE_END: bool, 7 const
RESET: char, 8 S>
---
(b) Recv type

⬇ 1MeshedChannels< 2 Recv<Data, 3 ’a’,6,true,7,true,’a’,End>, 4 Send<Data, 5
’b’,6,true,7,true,’b’,End>, 6 RoleSen<RoleSer<End>>, 7 NameSat, 8>
---
(c) MeshedChannels type for
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$

Figure 2: Main types of $\texttt{MultiCrusty}^{T}$

To augment the theory, we introduce the $\texttt{MultiCrusty}^{T}$ library, a
toolchain for implementing communication protocols in Rust.
$\texttt{MultiCrusty}^{T}$ specifies protocols where communication operations
must adhere to specific time limits (_timed_), allowing for _asynchronous_
message reception and runtime handling of certain failures (_affine_). This
library relies on two fundamental types: Send and Recv, representing message
sending and receiving, respectively. Additionally, it incorporates the End
type, signifying termination to close the connection. Figs. 2(a) and 2(b)
illustrate the Send and Recv types respectively, used for sending and
receiving messages of any thread-safe type (represented as T in Line 1). After
sending or receiving a message, the next operation or continuation (S in Line
8) is determined, which may entail sending another message, receiving another
message, or terminating the connection.

Similar to ATMP, each communication operation in $\texttt{MultiCrusty}^{T}$
is constrained by specific time boundaries to avoid infinite waiting. These
time bounds are represented by the parameters in Lines 2 to 7 of Fig. 2(a),
addressing scenarios where a role may be required to send after a certain time
unit or receive between two specific time units. Consider the final
communication operation in the first branch of Fig. 1(b) from
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$’s
perspective. To remain consistent with § 2.1, the communication is terminated
here instead of looping back to the beginning of the protocol. In this
operation,
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
sends a message labelled Data to
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
between time units $6$ and $7$, with respect to its inner clock ’b’, and then
terminates after resetting its clock. This can be implemented as: Send<Data,
’b’, 6, true, 7, true, ’b’, End>.

To enable multiparty communication in $\texttt{MultiCrusty}^{T}$, we use the
MeshedChannels type, inspired by [32]. This choice is necessary as Send and
Recv types are primarily designed for _binary_ (peer-to-peer) communication.
Within MeshedChannels, each binary channel pairs the owner role with another,
establishing a mesh of communication channels that encompasses all
participants. Fig. 2(c) demonstrates an example of using MeshedChannels for
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
in our running example:
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sat}}}$
receives a Data message from
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Sen}}}$
(Line 2) and forwards it to
$\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{Ser}}}$
(Line 4) before ending all communications, following the order specified by
the stack in Line 6.

Creating these types manually in Rust can be challenging and error-prone,
especially because they represent the local perspective of each role in the
protocol. Therefore, as depicted in Fig. 1(a) (right),
$\texttt{MultiCrusty}^{T}$ employs a top-down methodology similar to ATMP to
generate local viewpoints from a global protocol, while ensuring the
_correctness_ of the generated types _by construction_. To achieve this, we
extend the syntax of $\nu$Scr [50], a language for describing multiparty
communication protocols, to include time constraints, resulting in $\nu$ScrT.
A timed global protocol represented in $\nu$ScrT is then projected onto local
types, which are used for generating Rust types in
$\texttt{MultiCrusty}^{T}$.

##  3 Affine Timed Multiparty Session Calculus

In this section, we formalise an affine timed multiparty session
$\pi$-calculus, where processes are capable of performing time actions,
raising timeouts, and handling failures. We start with the formal definitions
of time constraints used in the paper.

#### Clock Constraint, Valuation, and Reset

Our time model is based on the timed automata formalism [1, 31]. Let
$\mathbf{C}$ denote a finite set of _clocks_ , ranging over
$C,C^{\prime},C_{1},\ldots$, that take non-negative real values in
$\mathbb{R}_{\geq 0}$. Additionally, let
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t^{\prime}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t_{1}},\ldots$
be _time constants_ ranging over $\mathbb{R}_{\geq 0}$. A _clock constraint_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}$
over $\mathbf{C}$ is defined as:

$\small{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}\,\Coloneqq\,\texttt{true}\mathbin{\;\big{|}\;}C>\mathfrak{b}\mathbin{\;\big{|}\;}C=\mathfrak{b}\mathbin{\;\big{|}\;}\neg{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}\mathbin{\;\big{|}\;}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}_{1}\land{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}_{2}$

where $C\in\mathbf{C}$ and $\mathfrak{b}$ is a _constant time bound_ ranging
over non-negative rationals $\mathbb{Q}_{\geq 0}$. We define
$\texttt{false},<,\geq,\leq$ in the standard way. For simplicity and
consistency with our implementation (§ 5), we assume each clock constraint
contains a _single_ clock. Extending a clock constraint with _multiple_ clocks
is straightforward.

A _clock valuation_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}}:\mathbf{C}\rightarrow\mathbb{R}_{\geq
0}$ assigns time to each clock in $\mathbf{C}$. We define
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}}+t$
as the valuation that assigns to each $C\in\mathbf{C}$ the value
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}}(C)+t$.
The _initial_ valuation that maps all clocks to $0$ is denoted as
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}}^{0}$,
and the valuation that assigns a value of $t$ to all clocks is denoted as
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}}^{t}$.
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}}\models{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}$
indicates that the constraint
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}$ is
satisfied by the valuation
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}}$.
Additionally, we use $\sqcup_{i\in
I}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}_{i}}$
to represent the overriding union of the valuations
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}_{i}}$
for $i\in I$.

A  _reset predicate_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\lambda}$
over $\mathbf{C}$ is a subset of $\mathbf{C}$ that defines the clocks to be
reset. If
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\lambda}=\emptyset$,
no reset is performed. Otherwise, the valuation for each clock
$C\in{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\lambda}$
is set to $0$. For clarity, we represent a reset predicate as $C:=0$ when a
single clock $C$ needs to be reset. To denote the clock valuation identical to
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}}$
but with the values of clocks in
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\lambda}$
to $0$, we use
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{V}}{}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\lambda}\mapsto
0]$.

#### Syntax of Processes

Our session $\pi$-calculus for affine timed multiparty session types (ATMP)
models timed processes interacting via affine meshed multiparty channels. It
extends the calculus for affine multiparty session types (AMPST) [32] by
incorporating asynchronous communication, time features, timeouts, and failure
handling.111 To simplify, our calculus exclusively emphasises send/receive
communication channels. Standard extensions, e.g. integers, booleans, and
conditionals, can easily integrate into our framework since they are
independent of our main formulation; they will be used in the examples.

######  Definition 3.1 (Syntax).

Let
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}},{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}},{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}},\ldots$
denote _roles_ belonging to a (fixed) set
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathcal{R}}$;
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s^{\prime}},\ldots$
for _sessions_ ; $x,y,\ldots$ for _variables_ ;
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}^{\prime}},\ldots$
for _message labels_ ; and
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}X},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Y},\ldots$
for _process variables_. The _affine timed multiparty session_ _$\pi$
-calculus_ syntax is defined as follows:

$\small\begin{array}[]{r@{\hskip 2mm}c@{\hskip 2mm}l@{\hskip
2mm}l}\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}d}\hskip
5.69054pt&\Coloneqq\hfil\hskip
5.69054pt&{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}x}\mathbin{\;\big{|}\;}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}\hfil\hskip
5.69054pt&\mbox{\small(variable, channel with role
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}$)}\\\\[2.84526pt]
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}\hskip
5.69054pt&\Coloneqq\hfil\hskip
5.69054pt&{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbf{0}}\mathbin{\;\big{|}\;}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}\mathbin{\;\big{|}\;}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\left(\mathbf{\nu}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\right){{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}\hfil\hskip
5.69054pt&\mbox{\small(inaction, parallel composition, restriction)}\\\ \hskip
5.69054pt&\hfil\hskip
5.69054pt&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]\mathbin{\\!\oplus\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}d}}\rangle\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]\mathbin{\\!\oplus\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}d}}\rangle\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]\mathbin{\\!\oplus\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}d}}\rangle\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]\mathbin{\\!\oplus\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}d}}\rangle\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}}$}}\hfil\hskip
5.69054pt&\mbox{\small(timed selection towards role
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}$)}\\\
\hskip 5.69054pt&\hfil\hskip
5.69054pt&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}$}}\hfil\hskip
5.69054pt&\mbox{\small(timed branching from role
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}$
with $I\neq\emptyset$)}\\\ \hskip 5.69054pt&\hfil\hskip
5.69054pt&{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbf{def}\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}D}}\;\mathbf{in}\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}\mathbin{\;\big{|}\;}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}X}}\\!\left\langle{\widetilde{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}}\right\rangle}\hfil\hskip
5.69054pt&\mbox{\small(process definition, process call)}\\\ \hskip
5.69054pt&\hfil\hskip
5.69054pt&\emph{\mbox{$\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}$}}\mathbin{\;\big{|}\;}\emph{\mbox{\textul{$\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}$}}}\hfil\hskip
5.69054pt&\mbox{\small(time-consuming delay, \textul{deterministic delay})}\\\
\hskip 5.69054pt&\hfil\hskip
5.69054pt&\mbox{\textul{$\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]$}}$}}\mathbin{\;\big{|}\;}\emph{\mbox{${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{try}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}\
\operatorname{\text{{catch}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}$}}\hfil\hskip
5.69054pt&\mbox{\small(\textul{timeout failure}, try-catch)}\\\ \hskip
5.69054pt&\hfil\hskip 5.69054pt&\emph{
\mbox{${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{cancel}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}\mathbin{\;\big{|}\;}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathsf{cerr}}}\mathbin{\;\big{|}\;}\mbox{\textul{${{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$}}\hfil\hskip
5.69054pt&\mbox{\small(cancel, communication error, \textul{kill})}\\\ \hskip
5.69054pt&\hfil\hskip
5.69054pt&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}$}}\hfil\hskip
5.69054pt&\mbox{\small(output message queue of role
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}$
in session
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}$)}\\\\[2.84526pt]
{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}D}\hskip
5.69054pt&\Coloneqq\hfil\hskip
5.69054pt&{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}X}}(\widetilde{x})={P}}\hfil\hskip
5.69054pt&\mbox{\small(declaration of process variable
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}X}$)}\\\\[2.84526pt]
\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}$}}\hskip
5.69054pt&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle\Coloneqq$}}{\hbox{\pagecolor{yellow!40}$\textstyle\Coloneqq$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle\Coloneqq$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle\Coloneqq$}}\hfil\hskip
5.69054pt&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}{!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle}}\mathrel{\\!\cdot\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}{!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle}}\mathrel{\\!\cdot\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}{!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle}}\mathrel{\\!\cdot\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}{!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle}}\mathrel{\\!\cdot\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}$}}\mathbin{\;\big{|}\;}\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\epsilon}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\epsilon}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\epsilon}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\epsilon}$}}\hfil\hskip
5.69054pt&\mbox{\small(message queue, non-empty or empty)}\end{array}$

Restriction, branching, and process definitions and declarations act as
binders;
$\operatorname{fc}\\!\left({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}\right)$
is the set of _free channels with roles_ in
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}$,
$\operatorname{fv}\\!\left({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}\right)$
is the set of _free variables_ in
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}$, and
$\Pi_{i\in
I}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}$ is
the parallel composition of processes
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}$.
Extensions w.r.t. _AMPST_ calculus are highlighted. Runtime processes,
generated dynamically during program execution rather than explicitly written
by users, are underlined.

Our calculus comprises:

_Channels_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c},{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}d}$,
being either variables
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}x}$ or
channels with roles (a.k.a. session _endpoints_)
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}$.

_Standard_ processes as in [43, 32], including inaction
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbf{0}}$,
parallel composition
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}$,
session scope restriction
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\left(\mathbf{\nu}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\right){{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$,
process definition
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbf{def}\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}D}}\;\mathbf{in}\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$,
process call
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}X}}\\!\left\langle{\widetilde{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}}\right\rangle}$,
and communication error
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathsf{cerr}}}$.

_Time_ processes that follow the program time behaviour of Fig. 2(c):

  * •

_Timed selection_ (or _timed internal choice_)
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]\mathbin{\\!\oplus\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}d}}\rangle\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}}$
indicates that a message
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}$
with payload
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}d}$ is sent
to role
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}$
via endpoint
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}$,
whereas _timed branching_ (or _timed external choice_)
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}$
waits to receive a message
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}$
from role
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}$
via endpoint
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}$ and
then proceeds as
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}$.

The parameter $\mathfrak{n}$ in both timed selection and branching is a
_timeout_ that allows modelling different types of communication primitives:
_blocking with a timeout_ ($\mathfrak{n}\in\mathbb{R}_{>0}$), _blocking_
($\mathfrak{n}=\infty$), or _non-blocking_ ($\mathfrak{n}=0$). When
$\mathfrak{n}\in\mathbb{R}_{\geq 0}$, the timed selection (or timed branching)
process waits for up to $\mathfrak{n}$ time units to send (or receive) a
message. If the message cannot be sent (or received) within this time, the
process moves into a _timeout state_ , raising a _time failure_. If
$\mathfrak{n}$ is set to $\infty$, the timed selection (or timed branching)
process blocks until a message is successfully sent (or received).

In our system, we allow  _send_ processes to be time-consuming, enabling
processes to wait before sending messages. Consider the remote data example
shown in Fig. 1(b). This practical scenario illustrates how a process might
wait before sending a message, resulting in the possibility of send actions
failing due to timeouts. It highlights the importance of timed selection,
contrasting with systems like in [5] where send actions are instantaneous.

  * •

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$
represents a _time-consuming delay_ action, such as method invocation or
sleep. Here,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}$ is
a clock constraint involving a _single_ clock variable $C$, used to specify
the interval for the delay. When executing
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$, any
time value
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}$ that
satisfies the constraint
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}$
can be consumed. Consequently, the _runtime_ _deterministic delay_ process
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$,
arising during the execution of
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$, is
introduced. In
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}$ is a
constant and a solution to
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}$,
and ${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}$ is
executed after a precise delay of
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}$ time
units.

  * •

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]$
signifies that the process
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}$ has
violated a time constraint, resulting in a _timeout failure_.

_Failure-handling_ processes that adopt the AMPST approach [32]:

  * •

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{try}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}\
\operatorname{\text{{catch}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}$
consists of a
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{try}}}}$
process ${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}$
that is prepared to communicate with a parallel composed process, and a
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{catch}}}}$
process
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}$, which
becomes active in the event of a cancellation or timeout. For clarity,
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{try}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbf{0}}}\
\operatorname{\text{{catch}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}$ is
not allowed within our calculus.

  * •

${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{cancel}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$
performs the _cancellation_ of other processes with channel
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}c}$.

  * •

${{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$
_kills_ (terminates) all processes with session
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}$, and is
dynamically generated only at _runtime_ from timeout failure or cancel
processes.

_Message queues_ :
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}$
represents the _output message queue_ of role
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}$
in session
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}$. It
contains all the messages previously sent by
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}$.
The queue
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}$
can be a sequence of messages of the form
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}{!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle}$,
where
${\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}$
is the receiver, or
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\epsilon}$,
indicating an _empty_ message queue. The set of _receivers in_
${\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}$,
denoted as
$\operatorname{receivers}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma})$,
is defined in a standard way as:

$\small\operatorname{receivers}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}{!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle}}\mathrel{\\!\cdot\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma^{\prime}}}})=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}\right\\}}}\cup\operatorname{receivers}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma^{\prime}})\quad\quad\operatorname{receivers}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\epsilon})=\emptyset$

$\begin{array}[]{c}\begin{array}[]{rl}{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[R-Out]}}&{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{E}}}\\!\left[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}}}]\mathbin{\\!\oplus\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s^{\prime}}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}}}\right]\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}\;\rightarrowtail\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}\mathrel{\\!\cdot\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}{!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s^{\prime}}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle}}\mathrel{\\!\cdot\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\epsilon}}}}}}}\\\\[1.42262pt]
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[R-In]}}&{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{E}}}\\!\left[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}}\right]\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}{!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{k}}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s^{\prime}}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle}}\mathrel{\\!\cdot\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}}}\;\rightarrowtail\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{k}}\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\nicefrac{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s^{\prime}}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}x_{k}}}}}\right\\}}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}\hskip
45.5244pt\text{\footnotesize($k\\!\in\\!I$) }\\\\[1.42262pt]
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[R-Err]}}&{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{E}}}\\!\left[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}}\right]\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}{!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}}\langle{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s^{\prime}}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}}\rangle}}\mathrel{\\!\cdot\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}}}\;\rightarrowtail\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathsf{cerr}}}\hskip
83.36658pt\text{\footnotesize($\forall
i\\!\in\\!I:{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}\neq{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{m}}$)
}\\\\[1.42262pt]
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[R-Det]}}&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle\models{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}{}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}/C]\;\;\text{implies}\;\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{E}}}\\!\left[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}}\right]\;\rightarrowtail\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}{\hbox{\pagecolor{yellow!40}$\textstyle\models{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}{}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}/C]\;\;\text{implies}\;\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{E}}}\\!\left[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}}\right]\;\rightarrowtail\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle\models{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}{}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}/C]\;\;\text{implies}\;\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{E}}}\\!\left[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}}\right]\;\rightarrowtail\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle\models{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}{}[{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}/C]\;\;\text{implies}\;\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{E}}}\\!\left[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\delta}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}}\right]\;\rightarrowtail\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{delay}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}}$}}\\\\[1.42262pt]
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[R-Time]}}&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}\;\rightharpoonup\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\Psi_{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P})}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}\;\rightharpoonup\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\Psi_{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P})}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}\;\rightharpoonup\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\Psi_{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P})}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}\;\rightharpoonup\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\Psi_{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}t}}({\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P})}$}}\\\\[1.42262pt]
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[R-Fail]}}&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]\;\rightarrowtail\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]\;\rightarrowtail\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]\;\rightarrowtail\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]\;\rightarrowtail\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$}}\hskip
191.2025pt\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle\text{\footnotesize($\exists{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}.\,{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\operatorname{subjP}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}})}=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}\right\\}}}$)}$}}{\hbox{\pagecolor{yellow!40}$\textstyle\text{\footnotesize($\exists{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}.\,{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\operatorname{subjP}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}})}=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}\right\\}}}$)}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle\text{\footnotesize($\exists{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}.\,{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\operatorname{subjP}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}})}=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}\right\\}}}$)}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle\text{\footnotesize($\exists{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}.\,{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\operatorname{subjP}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}})}=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}\right\\}}}$)}$}}\\\\[1.42262pt]
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[R-Can]}}&{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathbb{E}}}\\!\left[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{cancel}}}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}})}{\
\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}}\right]\;\rightarrowtail\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}\\\\[1.42262pt]
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[R-FailCat]}}&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{try}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]}\
\operatorname{\text{{catch}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}\;\rightarrowtail\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{try}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]}\
\operatorname{\text{{catch}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}\;\rightarrowtail\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{try}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]}\
\operatorname{\text{{catch}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}\;\rightarrowtail\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{try}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\boldsymbol{\mathtt{timeout}}}[{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}]}\
\operatorname{\text{{catch}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}\;\rightarrowtail\;{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}$}}\hskip
122.34685pt\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle\text{\footnotesize($\exists{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}.\,{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\operatorname{subjP}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}})}=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}\right\\}}}$)}$}}{\hbox{\pagecolor{yellow!40}$\textstyle\text{\footnotesize($\exists{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}.\,{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\operatorname{subjP}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}})}=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}\right\\}}}$)}$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle\text{\footnotesize($\exists{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}.\,{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\operatorname{subjP}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}})}=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}\right\\}}}$)}$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle\text{\footnotesize($\exists{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}.\,{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\operatorname{subjP}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}})}=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}\right\\}}}$)}$}}\\\\[1.42262pt]
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[C-Cat]}}&{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\operatorname{\text{{try}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}}\
\operatorname{\text{{catch}}}\
{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning\;\rightarrowtail\;{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}Q}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning\hskip
144.25546pt\text{\footnotesize($\exists{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}.\,{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\operatorname{subjP}({{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P}})}=\mathord{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@gray@stroke{0}\pgfsys@color@gray@fill{0}\left\\{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{r}}}}}]}\right\\}}}$)}\\\\[1.42262pt]
{\color[rgb]{0.1,0.3,0.1}\definecolor[named]{pgfstrokecolor}{rgb}{0.1,0.3,0.1}\textsc{\scriptsize[C-In]}}&\mathchoice{\hbox{\pagecolor{yellow!40}$\displaystyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$}}{\hbox{\pagecolor{yellow!40}$\textstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$}}{\hbox{\pagecolor{yellow!40}$\scriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$}}{\hbox{\pagecolor{yellow!40}$\scriptscriptstyle{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{p}}}}}]}}^{\mathfrak{n}}[\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}}}]}\mathbin{\\!\sum_{i\in
I}\\!}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mathtt{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{\mathtt{m}}_{\mathnormal{i}}}}}({x_{i}})\vphantom{x}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\\!.\\!}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}P_{i}}}}}{}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}[{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\boldsymbol{{\color[rgb]{0.5,0.0,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{0.5,0.0,0.0}\mathtt{q}}}}}]}}\mathrel{\\!\blacktriangleright\\!}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\sigma}}}\mathbin{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}\mid}}{{\color[rgb]{0,0,0}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0}s}}\lightning$}}\\\
&\hskip