Asynchronous Timed Session Types
Abstract
We present a behavioural typing system for a higherorder timed calculus using session types to model timed protocols. Behavioural typing ensures that processes in the calculus perform actions in the timewindows prescribed by their protocols. We introduce duality and subtyping for timed asynchronous session types. Our notion of duality allows typing a larger class of processes with respect to previous proposals. Subtyping is critical for the precision of our typing system, especially in the presence of session delegation. The composition of dual (timed asynchronous) types enjoys progress when using an urgent receive semantics, in which receive actions are executed as soon as the expected message is available. Our calculus increases the modelling power of extant calculi on timed sessions, adding a blocking receive primitive with timeout and a primitive that consumes an arbitrary amount of time in a given range.
Keywords
Session types Timers Duality \(\pi \)calculus1 Introduction
A calculus for timed asynchronous processes. Our calculus features two timesensitive primitives. The first is a parametric receive operation \(a^{n}(b).\, P\) on a channel a, with a timeout n that can be \(\infty \) or any number in \(\mathbf {R}_{\geqslant 0}\). The parametric receive captures a range of receive primitives: nonblocking (\(n=0\)), blocking without timeout (\(n=\infty \)), or blocking with timeout (\(n\in \mathbf {R}_{> 0}\)). The second primitive is a timeconsuming action, \(\mathtt {delay}(\delta ).\, P\), where \(\delta \) is a constraint expressing the timewindow for the time consumed by that action. Delay processes model primitives like \(\mathtt {Thread.sleep}(n)\) in realtime Java [13] or, more generally, any timeconsuming action, with \(\delta \) being an estimation of the delay of computation.
A type system for timed asynchronous processes. The relationship between types and processes in our calculus is given as a typing system. Welltyped processes are ensured to communicate at the times prescribed by their types. This result is given via Subject Reduction (Theorem 4), establishing that welltypedness is preserved by reduction. In our timed scenario, Subject Reduction holds under receive liveness, an assumption on the interaction structure of processes. This assumption is orthogonal to time. To characterise the interaction structures of a timed process we erase timing information from that processes (time erasure). Receive liveness requires that, whenever a timeerased processes is waiting for a message, the corresponding message is eventually provided by the rest of the system. While receive liveness is not needed for Subject Reduction in untimed systems [21], it is required for timed processes. This reflects the natural intuition that if an untimedprocess violates progress, then its timed counterpart may miss deadlines. Notably, we can rely on existing behavioural checking techniques from the untimed setting to ensure receive liveness [17].
Receive liveness is not required for Subject Reduction in a related work on asynchronous timed session types [12]. The dissimilarity in the assumptions is only apparent; it derives from differences in the two semantics for processes. When our processes cannot proceed correctly (e.g., in case of missed deadlines) they reduce to a failed state, whereas the processes in [12] become stuck (indicating violation of progress).
Synopsis. In Sect. 2 we introduce the syntax and the formation rules for asynchronous timed session types. In Sect. 3, we give a modular Labelled Transition System (LTS) for types in isolation (Sect. 3.1) and for compositions of types (Sect. 3.3). The subtyping relation is given in Sect. 3.2 and motivated in Example 8, after introducing the typing rules. We introduce timed asynchronous duality and its properties in Sect. 4. Remarkably, the composition of dual timed asynchronous types enjoys progress when using an urgent receive semantics (Theorem 1). Section 5 presents a calculus for timed processes and Sect. 6 introduces its typing system. The properties of our typing system—Subject Reduction (Theorem 4) and Time Safety (Theorem 5)—are introduced in Sect. 7. Conclusions and related works are in Sect. 8. Proofs and additional material can be found in the online report [11].
2 Asynchronous Timed Session Types
Clock valuation and resets. A clock valuation \(\nu : \mathbb {X}\mapsto \mathbf {R}_{\geqslant 0}\) returns the time of the clocks in \(\mathbb {X}\). We write \(\nu +t\) for the valuation mapping all \(x\in \mathbb {X}\) to \(\nu (x)+t\), \(\nu _0\) for the initial valuation (mapping all clocks to 0), and, more generally, \(\nu _t\) for the valuation mapping all clocks to t. Let \(\nu \models \delta \) denote that \(\delta \) is satisfied by \(\nu \). A reset predicate \(\lambda \) over \(\mathbb {X}\) is a subset of \(\mathbb {X}\). When \(\lambda \) is Open image in new window then no reset occurs, otherwise the assignment for each \(x\in \lambda \) is set to 0. We write \(\nu \, [\lambda \mapsto 0]\) for the clock assignment that is like \(\nu \) everywhere except that its assigns 0 to all clocks in \(\lambda \).
Type Open image in new window models a send action of a payload with sort \(T\). The sending action is allowed at any time that satisfies the guard \(\delta \). The clocks in \(\lambda \) are reset upon sending. Type Open image in new window models the dual receive action of a payload with sort \(T\). The receiving types require the endpoint to be ready to receive the message in the precise time window specified by the guard.
Type Open image in new window is a select action: the party chooses a branch \(i\in I\), where I is a finite set of indices, selects the label \(l_i\), and continues as prescribed by \(S_i\). Each branch is annotated with a guard \(\delta \) and reset \(\lambda \). A branch j can be selected at any time allowed by \(\delta _j\). The dual type is Open image in new window for branching actions. Each branch is annotated with a guard and a reset. The endpoint must be ready to receive the label for j at any time allowed by \(\delta _j\) (or until another branch is selected).
Recursive type \(\mu \alpha . S\) associates a type variable \(\alpha \) to a recursion body \(S\). We assume that type variables are guarded in the standard way (i.e., they only occur under actions or branches). We let \(\mathcal {A}\) denote the set of type variables.
Type \(\mathtt {end}\) models successful termination.
2.1 Type Formation
The grammar for types allow to generate types that are not implementable in practice, as the one shown in Example 1.
Example 1 (Junktypes)
In the remainder of this section we introduce formation rules to rule out junk types as the one in Example 1 and characterise types that are wellformed. Intuitively, wellformed types allow, at any point, to perform some action in the present time or at some point in the future, unless the type is \(\mathtt {end}\).
Rule \({~[\mathtt {end}]~}\) states that the terminated type is wellformed against any A. The guard of the judgement is \(\mathtt {true}\) since \(\mathtt {end}\) is a final state (as \(\mathtt {end}\) has no continuation, morally, the constraint of its continuation is always satisfiable). Rule \({~[\mathtt {interact}]~}\) ensures that the past of the current action \(\delta \) entails the past of the subsequent action \(\gamma \) (considering resets if necessary): this rules out types in which the subsequent action can only be performed in the past. Rules \({~[\mathtt {end}]~}\) and \({~[\mathtt {interact}]~}\) are illustrated by the three examples below.
Example 2
Rule \({~[\mathtt {delegate}]~}\) behaves as \({~[\mathtt {interact}]~}\), with two additional premises on the delegated session: (1) \(S'\) needs to be wellformed, and (2) the guard of the next action in \(S'\) needs to be satisfiable with respect to \(\delta '\). Guard \(\delta '\) is used to ensure a correspondence between the state of the delegating endpoint and that of the receiving endpoint. Rule \({~[\mathtt {choice}]~}\) is similar to \({~[\mathtt {interact}]~}\) but requires that there is at least one viable branch (this is accomplished by considering the weaker past \(\mathbin {\downarrow {\bigvee }}_{i\in I}\delta _i\)) and checking each branch for formation. Rules \({~[\mathtt {rec}]~}\) and \({~[\mathtt {var}]~}\) are for recursive types and variables, respectively. In \( {~[\mathtt {rec}]~}\) the guard \(\delta \) can be easily computed by taking the past of the next action of the in \(S\) (or the disjunction if \(S\) is a branching or selection). An algorithm for deciding type formation can be found in [11].
Definition 1 (Wellformed types)
We say that \(S\) is wellformed against clock valuation \(\nu \) if Open image in new window and \(\nu \models \delta \), for some guard \(\delta \). We say that \(S\) is wellformed if it is well formed against \(\nu _0\).
We will tacitly assume types are wellformed, unless otherwise specified. The intuition of wellformedness is that if \(A ; \ \delta \, \vdash \,S\) then \(S\) can be run (using the types semantics given in Sect. 3) under any clock valuation \(\nu \) such that \(\nu \models \delta \). In the sequel, we take (wellformed) types equirecursively [31].
3 Asynchronous Session Types Semantics and Subtyping
3.1 Types in Isolation
Let \(\mathbf {s}\), \(\mathbf {s}'\), \(\mathbf {s}_i\) (\(i\in \mathbb {N}\)) range over simple type configurations \((\nu , S)\). We write \(\mathbf {s}{\mathop {\longrightarrow }\limits ^{\ell }}\) when there exists \(\mathbf {s}'\) such that \(\mathbf {s}{\mathop {\longrightarrow }\limits ^{\ell }}\mathbf {s}'\), and write \(\mathbf {s}{\mathop {\longrightarrow }\limits ^{t \, \ell }}\) for \(\mathbf {s}{\mathop {\longrightarrow }\limits ^{t}} {\mathop {\longrightarrow }\limits ^{\ell }}\).
3.2 Asynchronous Timed Subtyping
We define subtyping as a partial relation on simple type configurations. As in other subtyping relations for session types we consider send and receive actions dually [14, 16, 19]. Our subtyping relation is covariant on output actions and contravariant on input actions, similarly to that of [14]. In this way, our subtyping \(S <\,:S'\) captures the intuition that a process welltyped against S can be safely substituted with a process welltyped against \(S'\). Definition 2, introduces a notation that is useful in the rest of this section.
Definition 2 (Future enabled send/receive)
Action \(\ell \) is future enabled in \(\mathbf {s}\) if \(\exists t: \mathbf {s}{\mathop {\longrightarrow }\limits ^{t \, \ell }}\). We write \(\mathbf {s} {\mathop {\Rightarrow }\limits ^{!}}\) (resp. \(\mathbf {s} {\mathop {\Rightarrow }\limits ^{?}}\)) if there exists a sending action !m (resp. a receiving action ?m) that is future enabled in \(\mathbf {s}\).
As common in session types, the communication structure does not allow for mixed choices: the grammar of types enforces choices to be either all input (branching actions), or output (selection actions). From this fact it follows that, given \(\mathbf {s}\), reductions \(\mathbf {s} {\mathop {\Rightarrow }\limits ^{!}}\) and \(\mathbf {s} {\mathop {\Rightarrow }\limits ^{?}}\) cannot hold simultaneously.
Definition 3 (Timed Type Simulation)
 1.
\(S_1 = \mathtt {end}\) implies \(S_2 = \mathtt {end}\)
 2.
\(\mathbf {s}_1 {\mathop {\longrightarrow }\limits ^{t \, !m_1}}\mathbf {s}_1'\) implies \(\exists \mathbf {s}_2',m_2:\mathbf {s}_2{\mathop {\longrightarrow }\limits ^{t \, !m_2}}\mathbf {s}_2'\), \((m_2,m_1) \in \mathcal {S}, (\mathbf {s}_1',\mathbf {s}_2')\in \mathcal {R}\)
 3.
\(\mathbf {s}_2{\mathop {\longrightarrow }\limits ^{t \, ?m_2}}\mathbf {s}_2'\) implies \(\exists \mathbf {s}_1',m_1: \mathbf {s}_1{\mathop {\longrightarrow }\limits ^{t \, ?m_1}}\mathbf {s}_1'\), \((m_1,m_2) \in \mathcal {S}\), \((\mathbf {s}_1',\mathbf {s}_2')\in \mathcal {R}\)
 4.
\(\mathbf {s}_1 {\mathop {\Rightarrow }\limits ^{?}}\) implies \(\mathbf {s}_2 {\mathop {\Rightarrow }\limits ^{?}}\) and \(\mathbf {s}_2 {\mathop {\Rightarrow }\limits ^{!}}\) implies \(\mathbf {s}_1 {\mathop {\Rightarrow }\limits ^{!}}\)
Definition 4 (Live simple type configuration)
Observe that for all wellformed \(S\), \((\nu _0, S)\) is live.
Subtyping for simple type configurations. We can now define subtyping for simple type configurations and state its decidability.
Definition 5 (Subtyping)
\(\mathbf {s}_1\) is a subtype of \(\mathbf {s}_2\), written \(\mathbf {s}_1 <\,:\mathbf {s}_2\), if there exists a timed type simulation \(\mathcal {R}\) on live simple type configurations such that \((\mathbf {s}_1,\mathbf {s}_2)\in \mathcal {R}\). We write \(S_1<\,:S_2\) when \((\nu _0, S_1) <\,:(\nu _0,S_2)\). Abusing the notation, we write \( m <\,:m'\) iff there exists \(\mathcal {S}\) such that \((m,m')\in \mathcal {S}\).
Subtyping has been shown to be decidable in the untimed setting [19] and in the timed first order setting [6]. In [6], decidability is shown through a reduction to model checking of timed automata networks. The result in [6] can be extended to higherorder messages using the techniques in [3], based on finite representations (called regions) of possibly infinite sets of clock valuations.
Proposition 1 (Decidability of subtyping)
Checking if \((\delta _1, S_1) <\,:(\delta _2, S_2)\) is decidable.
3.3 Types with Queues, and Their Composition
Composing types. Configurations are composed into systems. We denote \(\mathbf {S}\mid \mathbf {S}'\) as the parallel composition of the two configurations \(\mathbf {S}\) and \(\mathbf {S}'\).
Example 3 (A good communication)
Example 4 (In absence of urgency)
4 Timed Asynchronous Duality
We introduce a timed extension of duality. As in untimed duality, we let each send/select action be complemented by a corresponding receive/branching action. Moreover, we require time constraints and resets to match.
Definition 6 (Timed duality)
Duality with urgent receive semantics enjoys the following properties: systems with dual types fulfil progress (Theorem 1); behaviour (resp. progress) of a system is preserved by the substitution of a type with a subtype (Theorem 2) (resp. Theorem 3). A system enjoys progress if it reaches states that are either final or that allow further communications, possibly after a delay. Recall that we assume types to be wellformed (cf. Definition 1): Theorems 1, 2, and 3 rely on this assumption.
Definition 7 (Type progress)
Theorem 1 (Duality progress)
System Open image in new window enjoys progress.
We show that subtyping does not introduce new behaviour, via the usual notion of timed simulation [1]. Let \(\mathbf {c}, \mathbf {c}_1, \mathbf {c}_2\) range over systems. Fix \(\mathbf {c}_1= (\nu _1^1, S_1^1, \mathtt {M}_1^1)\mid (\nu _2^1, S_2^1, \mathtt {M}_2^1)\), and \(\mathbf {c}_2 = (\nu _1^2, S_1^2, \mathtt {M}_1^2)\mid (\nu _2^2, S_2^2, \mathtt {M}_2^2)\). We say that a binary relation over systems preserves \(\mathtt {end}\) if: Open image in new window iff Open image in new window for all \(i\in \{1,2\}\). Write \(\mathbf {c}_1 \lesssim \mathbf {c}_2\) if \((\mathbf {c}_1, \mathbf {c}_2)\) are in a timed simulation that preserves \(\mathtt {end}\).
Theorem 2 (Safe substitution)
If \(S' <\,:\overline{S}\), then Open image in new window .
Theorem 3 (Progressing substitution)
If \(S' <\,:\overline{S}\), then Open image in new window satisfies progress.
5 A Calculus for Asynchronous Timed Processes
Open image in new window sends a value v on channel \(a\) and continues as P. Similarly, Open image in new window sends a label Open image in new window on channel \(a\) and continue as P. Process Open image in new window behaves as either P or Q depending on the boolean value v. Process \(P\mid Q\) is for parallel composition of P and Q, and \(0\) is the idle process. \(\mathtt {def}\;D\;\mathtt {in}\;P\) is the standard recursive process: D is a declaration, and P is a process that may contain recursive calls. In recursive calls Open image in new window the first list of parameters has to be instantiated with values of ground types, while the second with channels. Recursive calls are instantiated with equations Open image in new window in D. Process \((\nu ab) P\) is for scope restriction of endpoints \(a\) and \(b\). Process \(ab: h\) is a queue with name \( ab\) (colloquially used to indicate that it contains messages in transit from \(a\) to \(b\)) and content \(h\). \((\nu ab)\) binds endpoints \( a\) and \(b\), and queues \( ab\) and \( ba\) in P.
There are two kind of timeconsuming processes: those performing a timeconsuming action (e.g., method invocation, sleep), and those waiting to receive a message. We model the first kind of processes with \(\mathtt {delay}(\delta ).\, P\), and the second kind of processes with Open image in new window (receive) and Open image in new window (branching). In \(\mathtt {delay}(\delta ).\, P\), \(\delta \) is a constraints as those defined for types, but on one single clock \(x\). The name of the clock here is immaterial: clock \(x\) is used as a syntactic tool to define intervals for the timeconsuming (delay) action. In this sense, assume x is bound in \(\mathtt {delay}(\delta ).\, P\). Process \(\mathtt {delay}(\delta ).\, P\) consumes any amount of time t such that t is a solution of \(\delta \). For example \(\mathtt {delay}(x\leqslant 3).\, P\) consumes any value between 0 to 3 time units, then behaves as P. Process \(a^{n}(b).\, P\) receive a message on channel \(a\), instantiates \(b\) and continue as P. Parameter \(n\) models different receive primitives: nonblocking (\(n=0\)), blocking (\(n=\infty \)), and blocking with timeout (\(n\in \mathbb {R}^{\geqslant 0}\)). If \(n\in \mathbb {R}^{\geqslant 0}\) and no message is in the queue, the process waits \(n\) time units before moving into a failed state. If \(n\) is set to \(\infty \) the process models a blocking primitive without timeout. Branching process Open image in new window is similar, but receives a label Open image in new window and continues as \(P_i\).
Runtime processes are not written by programmers and only appear upon execution. Process \(\mathtt {failed}\) is the process that has violated a time constraint. We say that P is a failed state if it has \(\mathtt {failed}\) as a syntactic subterm. Process \(\mathtt {delay}(t).\, P \) delays for exactly \(t\) time units.
Reduction for processes. Processes are considered modulo structural equivalence, denoted by \(\equiv \), and defined by adding the following rule for delays to the standard ones [28]: \(\mathtt {delay}(0).\, P\equiv P\). Reduction rules for processes are given in Fig. 3. A reduction step \(\longrightarrow \) can happen because of either an instantaneous step \(\rightharpoonup \) by \([\mathtt {Red1}]\) or timeconsuming step \(\rightsquigarrow \) by \([\mathtt {Red2}]\). Rules \([\mathtt {Send}]\), \([\mathtt {Rcv}]\), \([\mathtt {Sel}]\), and \([\mathtt {Bra}]\) are the usual asynchronous communication rules. Rule \([\mathtt {Det}]\) models the random occurrence of a precise delay t, with t being a solution of \(\delta \). The other untimed rules, \([\mathtt {IfT}]\), \([\mathtt {Par}]\), \([\mathtt {Def}]\), \([\mathtt {Rec}]\), \([\mathtt {AStr}]\), and \([\mathtt {AScope}]\) are standard. Note that rule \([\mathtt {Par}]\) does not allow time passing, which is handled by rule \([\mathtt {Delay}]\). Rule \([\mathtt {TStr}]\) is the timed version of \([\mathtt {AStr}]\). Rule \([\mathtt {Delay}]\) applies a timepassing function \(\varPhi _{t}\) (defined in Fig. 4) which distributes the delay t across all the parts of a process. \(\varPhi _{t}(P)\) is a partial function: it is undefined if P can immediately make an urgent action, such as evaluation of expressions or output actions. If \(\varPhi _{t}(P)\) is defined, it returns the process resulting from letting \(t\) time units elapse in P. \(\varPhi _t(P)\) may return a failed state, if delay t makes a deadline in P expire. The definition of \(\varPhi _t(P_1 \mid P_2)\) relies on two auxiliary functions: \(\mathtt {Wait}(P)\) and \(\mathtt {NEQueue}(P)\) (see [11] for the full definition). \(\mathtt {Wait}(P)\) returns the set of channels on which P (or some syntactic subterm of P) is waiting to receive a message/label. \(\mathtt {NEQueue}(P)\) returns the set of endpoints with a nonempty inbound queue. For example, Open image in new window and \(\mathtt {NEQueue}(ba: h)=\{a\}\) given that Open image in new window . \(\varPhi _t(P_1 \mid P_2)\) is defined only if no urgent action could immediately happen in \(P_1\mid P_2\). For example, \(\varPhi _t(P_1 \mid P_2)\) is undefined for \(P_1= a^{t}(b).\, Q\) and \(P_2=ba:v\).
In the rest of this section we show the reductions of two processes: one with urgent actions (Example 5), and one to a failed state (Example 6). We omit processes that are immaterial for the illustration (e.g., unused queues).
Example 5
Example 6
6 Typing for Asynchronous Timed Processes
Notation, assumptions, and auxiliary definitions. We write \(\varDelta + t\) for the session environment obtained by incrementing all clock valuations in the codomain of \(\varDelta \) by t.
Definition 8
 1.
If \(\varDelta \in \varTheta \) and \(\varDelta (a)=(\nu , S)\), then \(S\) is wellformed (Definition 1) against \(\nu \);
 2.
For all \(\varDelta _1 \in \varTheta \), \(\varDelta _2 \in \varTheta \): \(\mathtt {type}(\varDelta _1(a)) = S\) iff \(\mathtt {type}(\varDelta _2(a)) = S\);
 3.There is guard \(\delta \) such that:$$ \{\nu \mid \nu \models \delta \} = \bigcup _{\varDelta \in \varTheta } \mathtt {val}(\varDelta ). $$
The last condition ensures that \(\varTheta \) is finitely representable, and is key for decidability of type checking.
Example 7
In the following, we write \(\mathbf {a}:\mathbf {T}\) for \(a_1 : T_1, \ldots , a_n : T_n\) when \(\mathbf {a}= a_1 , \ldots , a_n \) and \(\mathbf {T}= T_1, \ldots , T_n\) (assuming \(\mathbf {a}\) and \(\mathbf {T}\) have the same number of elements). Similarly for \(\mathbf {b}:\mathbf {(\nu ,S)}\). In the typing rules, we use a few auxiliary definitions: Definition 9 (\(t\)reading \(\varDelta \)) checks if any ongoing sessions in a \(\varDelta \) can perform an input action within a given timespan, and Definition 10 (Compatibility of configurations) extends the notion of duality to systems that are not in an initial state.
Definition 9
(\(t\)reading \(\varDelta \)). Session environment \(\varDelta \) is \(t\)reading if there exist some \(a\in \mathrm {dom}(\varDelta )\), \(t' < t\) and m such that: \(\varDelta (a) = (\nu ,S) \wedge (\nu + t',S) {\mathop {\longrightarrow }\limits ^{?m}}\).
Namely, \(\varDelta \) is \(t\)reading if any of the open sessions in the mapping prescribe a read action within the timeframe between \(\nu \) and \(\nu +t\). Definition 9 is used in the typing rules for timeconsuming processes – \([\mathtt {Vrcv}]\), \([\mathtt {Drcv}]\), and \([\mathtt {Del\textit{t}}]\) – to ‘disallow’ derivations when a (urgent) receive may happen.
Definition 10
By condition (3) initial configurations are compatible when they include dual types, i.e., Open image in new window . By condition (2) two configurations may temporarily misalign as execution proceeds: one may have read a message from its queue, while the other has not, as long as the former is ready to receive it immediately. Thanks to the particular shape of type’s interactions, initial configurations – of the form Open image in new window – will only reach systems, say \((\nu _1,S_1, \mathtt {M}_1) \bot (\nu _2,{S_2}, \mathtt {M}_2)\), in which at least one between \(\mathtt {M}_1\) and \(\mathtt {M}_2\) is empty. Condition (1) requires compatible configurations to satisfy this basic property.

\(\nu + t\models \delta \Rightarrow t\leqslant n\) rules out processes that are not ready to receive a message when prescribed by the type.

\(t\leqslant n\Rightarrow \nu + t\models \delta \) requires that \(a^{n}(b).\, P\) can read only at times that satisfy the type prescription \(\delta \).^{2}
The second premise of \([\mathtt {Vrcv}]\) requires the continuation P to be welltyped against the continuation of the type, for all possible session environments where the virtual time is somewhere between \([\nu ,\nu +n]\), where the virtual valuation \(\nu \) in the mapping of session \(a\) is reset according to \(\lambda \). Rule \([\mathtt {Drcv}]\), for processes receiving delegated sessions, is like \([\mathtt {Vrcv}]\) except: (a) the continuation P is typed against a session environment extended with the received session \(S'\), and (b) the clock valuation \(\nu '\) of the receiving session must satisfy \(\delta '\). Recall that by formation rules (Sect. 2.1) \(S'\) is wellformed against all \(\nu '\) that satisfy \(\delta '\).
Rule \([\mathtt {Vsend}]\) is for output processes. Send actions are instantaneous, hence the type current \(\nu \) needs to satisfy \(\delta \). As customary, the continuation of the process needs to be welltyped against the continuation of the type (with \(\nu \) being reset according to \(\lambda \), and \(\varGamma \) extended with information on the sort of b). \([\mathtt {Dsend}]\) for delegation is similar but: (a) the delegated session is removed from the session environment (the process can no longer engage in the delegated session), and (b) valuation \(\nu '\) of the delegated session must satisfy guard \(\delta '\).
Rule \([\mathtt {Del\delta }]\) checks that P is welltyped against all possible solutions of \(\delta \). Rule \([\mathtt {Del\textit{t}}]\) shifts the virtual valuations in the session environment of \(t\). This is as the corresponding rule in [12] but with the addition of the check that \(\varDelta \) is not \(t\)reading, needed because of urgent semantics.
Rule \([\mathtt {Res}]\) is for processes with scopes.
Rule \([\mathtt {Rec}]\) is for recursive processes. The rule is as usual [21] except that we use a set of session environments \(\varTheta \) (instead of a single \(\varDelta \)) to capture a set of possible scenarios in which a recursion instance may start, which may have different clock valuations. Rule \([\mathtt {Var}]\) is also as expected except for the use of \(\varTheta \).
Rules \([\mathtt {Par}]\) and \([\mathtt {Subt}]\) straightforward.
Example 8 (Typing with subtyping)
7 Subject Reduction and Time Safety
The untimed calculus. We define untimed processes, denoted by \(\hat{P}\), as processes obtained from the grammar given for timed processes (Sect. 5) without delays and failed processes. In untimed processes, time annotations of branching/receive processes are immaterial, hence omitted in the rest of the paper.
Given a (timed) process P, one can obtain its untimed counterpart by erasing delays and failed processes; we denoted the result of such erasure on P by \(\mathtt {erase}(P)\). The semantics of untimed processes is defined as the one for timed processes (Sect. 5) except that reduction rules \([\mathtt {Delay}]\), \([\mathtt {TStr}]\), and \([\mathtt {Red2}]\), are removed. Abusing the notation, we write \(\hat{P}{\mathop {\longrightarrow }\limits ^{}} \hat{P'}\) when an untimed process \(\hat{P}\) moves to a state \(\hat{P'}\) using the semantics for untimed processes. The definitions of \(\mathtt {Wait}(\hat{P})\) and \(\mathtt {NEQueue}(\hat{P})\) can be derived from the definitions for timed processes in the straightforward way.
Definition 11 (receive liveness) formalises our assumption on the interaction structures of a process.
Definition 11 (Receive liveness)
In any reachable state \(\hat{P}'\) of a live untimed process \(\hat{P}\), if any endpoint a in \(\hat{P}'\) is waiting to receive a message (\(a\in \mathtt {Wait}(\hat{Q})\)), then the overall process is able to reach a state \(\hat{Q}'\) where a can perform the receive action (\(a\in \mathtt {NEQueue}(\hat{Q}')\)).
Consider process P in (13). The untimed process \(\mathtt {erase}(P)\) is not live because \(\mathtt {Wait}(\mathtt {erase}(P)) = \{a,c\}\) and \(a,c\not \in \mathtt {NEQueue}(\mathtt {erase}(P))\), since \(\mathtt {NEQueue}(\mathtt {erase}(P))\) is the empty set. Syntactically, \(\mathtt {erase}(P)\) is as P, but it does not have the same behaviour. P can only make time steps, reaching a failed process, while \(\mathtt {erase}(P)\) is stuck, as untimed processes only make communication steps.
Properties. Time safety relies on Subject Reduction Theorem 4, which establishes a relation (preserved by reduction) of welltyped processes and their types.
Theorem 4 (Subject reduction for closed systems)
Let \(\mathtt {erase}(P)\) be live. If Open image in new window and \(P ~~\longrightarrow ~~P'\) then Open image in new window .
Note that Subject Reduction assumes \(\mathtt {erase}(P)\) to be live. For instance, the example of P in (13) is welltyped, but \(\mathtt {erase}(P)\) is not live. The process can reduce to a failed state (as illustrated earlier in this section) that cannot be typed (failed processes are not welltyped). Time Safety establishes that welltyped processes only reduce to failfree states.
Theorem 5 (Time safety)
If \(\mathtt {erase}(P)\) is live, Open image in new window and \(P ~~\longrightarrow ^*~~P'\), then \(P'\) is failfree.
Typing is decidable if one uses processes annotated with the following information: (1) scope restrictions \((\nu ab:S) P\) are annotated with the type \(S\) of the session for endpoint \(a\) (the type of \(b\) is implicitly assumed to be \(\overline{S}\) and both endpoints are type checked in the initial clock valuation \(\nu _0\)); (2) receive actions \(a^{n}(b:T).\, P\) are annotated with the type \(T\) of the received message; (3) recursion \(X(\mathbf {a:T} \; ; \, \mathbf {a:S},\delta )=P\) are annotated with types for each parameter, and a guard modelling the state of the clocks. We call annotated programs those annotated processes derived without using productions marked as runtime (i.e., \(\mathtt {failed}\) and \(\mathtt {delay}(t).\, P\)), and where \(n\) in \(a^{n}(b:T).\, P\) ranges over \(\mathbb {Q}_{\geqslant 0} \cup \{\infty \}\).
Proposition 2
Type checking for annotated programs is decidable.
8 Conclusion and Related Work
We introduced duality and subtyping relations for asynchronous timed session types. Unlike for untimed and timed synchronous [6] dualities, the composition of dual types does not enjoy progress in general. Compositions of asynchronous timed dual types enjoy progress when using an urgent receive semantics. We propose a behavioural typing system for a timed calculus that features nonblocking and blocking receive primitives (with and without timeout), and time consuming primitives of arbitrary but constrained delays. The main properties of the typing system are Subject Reduction and Time Safety; both results rely on an assumption (receive liveness) of the underneath interaction structure of processes. In related work on timed session types [12], receive liveness is not required for Subject Reduction; this is because the processes in [12] block (rather than reaching a failed state) whenever they cannot progress correctly, hence e.g., missed deadline are regarded as progress violations. By explicitly capturing failures, our calculus paves the way for future work on combining static checking with runtime instrumentation to prevent or handle failures.
Asynchronous timed session types have been introduced in [12], in a multiparty setting, together with a timed \(\pi \)calculus, and a type system. The direct extension of session types with time introduces unfeasible executions (i.e., types may get stuck), as we have shown in Example 1. [12] features a notion of feasibility for choreographies, which ensures that types enjoy progress. We ensure progress of types by formation and duality. The semantics of types in [12] is different from ours in that receive actions are not urgent. The work in [12] gives one extra condition on types (waitfreedom), because feasible types may still yield undesirable executions in welltyped processes. Thanks to our duality, subtyping, and calculus (in particular the blocking receive primitive with timeout) this condition is unnecessary in this work. As a result, our typing system allows for types that are not waitfree. By dropping waitfreedom, we can type a class of common realworld protocols in which processes may be ready to receive messages even before the final deadline of the corresponding senders. Remarkably, SMTP mentioned in the introduction is not waitfree. For some other aspects, our work is less general than the one in [12], as we consider binary sessions rather than multiparty sessions. A theory of timed multiparty asynchronous protocols that encompasses the protocols in [12] and those considered here is an interesting future direction. The work in [6] introduces a theory of synchronous timed session types, based on a decidable notion of compatibility, called compliance, that ensures progress of types, and is equivalent to synchronous timed duality and subtyping in a precise sense [6]. Our duality and subtyping are similar to those in [6], but apply to the asynchronous scenario. The work in [15] introduces a typed calculus based on temporal session types. The temporal modalities in [15] can be used as a discrete model of time. Timed session types, thanks to clocks and resets, are able to model complex timed dependencies that temporal session types do not seem able to capture. Other work studies models for asynchronous timed interactions, e.g., Communicating Timed Automata [23] (CTA), timed Message Sequence Charts [2], but not their relationships with processes. The work in [5] introduces a refinement for CTA, and presents a notion of urgency similar to the one used in this paper, preliminary studied also in [29].
Several timed calculi have been introduced outside the context of behavioural types. The work in [32] extends the \(\pi \) calculus with time primitives inspired in CTA and is closer, in principle, to our types than our processes. Another timed extension of the \(\pi \)calculus with timeconsuming actions has been applied to the analysis the active times of processes [18]. Some works focus on specific aspects of timed behaviour, such as timeouts [9], transactions [24, 27], and services [25]. Our calculus does not feature exception handlers, nor timed transactions. Our focus in on detecting time violations via static typing, so that a process only moves to failfree states.
The calculi in [7, 12, 15] have been used in combination with session types. The calculus in [12] features a nonblocking receive primitive similar to our \(a^{0}(b).\, P\), but that never fails (i.e., time is not allowed to flow if a process tries to read from an empty buffer—possibly leading to a stuck process rather than a failed state). The calculus in [7] features a blocking receive primitive without timeout, equivalent to our \(a^{\infty }(b).\, P\). The calculus in [15], seems able to encode a nonblocking receive primitive like the one of [12] and a blocking receive primitive without timeout like our \(a^{\infty }(b).\, P\). None of these works features blocking receive primitives with timeouts. Furthermore, existing works feature [7, 12] or can encode [15] only precise delays, equivalent to \(\mathtt {delay}(x=n).\, P\). Such punctual predictions are often difficult to achieve. Arbitrary but constrained delays are closer abstractions of timeconsuming programming primitives (and possibly, of predictions one can derive by cost analysis, e.g., [20]).
As to applications, timed session types have been used for runtime monitoring [7, 30] and static checking [12]. A promising future direction is that of integrating static typing with runtime verification and enforcement, towards a theory of hybrid timed session types. In this context, extending our calculus with exception handlers [9, 24, 27] could allow an extension of the typing system, that introduces runtime instrumentation to handle unexpected time failures.
Footnotes
References
 1.Aceto, L., Ingólfsdóttir, A., Larsen, K.G., Srba, J.: Reactive Systems: Modelling, Specification and Verification. Cambridge University Press, Cambridge (2007). https://doi.org/10.1017/CBO9780511814105CrossRefzbMATHGoogle Scholar
 2.Akshay, S., Gastin, P., Mukund, M., Kumar, K.N.: Model checking timeconstrained scenariobased specifications. In: FSTTCS. LIPIcs, vol. 8, pp. 204–215. Schloss Dagstuhl  LeibnizZentrum fuer Informatik (2010). https://doi.org/10.4230/LIPIcs.FSTTCS.2010.204
 3.Alur, R., Dill, D.L.: A theory of timed automata. TCS 126, 183–235 (1994)MathSciNetCrossRefGoogle Scholar
 4.Advanced Message Queuing Protocols (AMQP). https://www.amqp.org/
 5.Bartoletti, M., Bocchi, L., Murgia, M.: Progresspreserving refinements of CTA. In: CONCUR. LIPIcs, vol. 118, pp. 40:1–40:19. Schloss DagstuhlLeibnizZentrum fuer Informatik (2018). https://doi.org/10.4230/LIPIcs.CONCUR.2018.40
 6.Bartoletti, M., Cimoli, T., Murgia, M.: Timed session types. Log. Methods Comput. Sci. 13(4) (2017). https://doi.org/10.23638/LMCS13(4:25)2017
 7.Bartoletti, M., Cimoli, T., Murgia, M., Podda, A.S., Pompianu, L.: A contractoriented middleware. In: Braga, C., Ölveczky, P.C. (eds.) FACS 2015. LNCS, vol. 9539, pp. 86–104. Springer, Cham (2016). https://doi.org/10.1007/9783319289342_5CrossRefGoogle Scholar
 8.Bengtsson, J., Yi, W.: Timed automata: semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004). https://doi.org/10.1007/9783540277552_3CrossRefzbMATHGoogle Scholar
 9.Berger, M., Yoshida, N.: Timed, distributed, probabilistic, typed processes. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 158–174. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540766377_11CrossRefGoogle Scholar
 10.Bettini, L., Coppo, M., D’Antoni, L., De Luca, M., DezaniCiancaglini, M., Yoshida, N.: Global progress in dynamically interleaved multiparty sessions. In: van Breugel, F., Chechik, M. (eds.) CONCUR 2008. LNCS, vol. 5201, pp. 418–433. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540853619_33CrossRefGoogle Scholar
 11.Bocchi, L., Murgia, M., Vasconcelos, V., Yoshida, N.: Asynchronous timed session types: from duality to timesensitive processes (2018). https://www.cs.kent.ac.uk/people/staff/lb514/tstp.html
 12.Bocchi, L., Yang, W., Yoshida, N.: Timed multiparty session types. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 419–434. Springer, Heidelberg (2014). https://doi.org/10.1007/9783662445846_29CrossRefGoogle Scholar
 13.Bruno, E.J., Bollella, G.: RealTime Java Programming: With Java RTS, 1st edn. Prentice Hall PTR, Upper Saddle River (2009)Google Scholar
 14.Chen, T.C., DezaniCiancaglini, M., Yoshida, N.: On the preciseness of subtyping in session types. In: PPDP, pp. 135–146. ACM (2014). https://doi.org/10.1145/2643135.2643138
 15.Das, A., Hoffmann, J., Pfenning, F.: Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang. 2(ICFP), 91:1–91:30 (2018). https://doi.org/10.1145/3236786CrossRefGoogle Scholar
 16.Demangeon, R., Honda, K.: Full abstraction in a subtyped picalculus with linear types. In: Katoen, J.P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 280–296. Springer, Heidelberg (2011). https://doi.org/10.1007/9783642232176_19CrossRefGoogle Scholar
 17.DezaniCiancaglini, M., de’Liguoro, U., Yoshida, N.: On progress for structured communications. In: Barthe, G., Fournet, C. (eds.) TGC 2007. LNCS, vol. 4912, pp. 257–275. Springer, Heidelberg (2008). https://doi.org/10.1007/9783540786634_18CrossRefGoogle Scholar
 18.Fischer, M., Förster, S., Windisch, A., Monjau, D., Balser, B.: A new time extension to \(\pi \)calculus based on time consuming transition semanticss. In: Grimm, C. (ed.) Languages for System Specification, pp. 271–283. Springer, Boston (2004). https://doi.org/10.1007/1402079915_17CrossRefGoogle Scholar
 19.Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Inf. 42(2–3), 191–225 (2005). https://doi.org/10.1007/s002360050177zMathSciNetCrossRefzbMATHGoogle Scholar
 20.Hoffmann, J., Shao, Z.: Automatic static cost analysis for parallel programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 132–157. Springer, Heidelberg (2015). https://doi.org/10.1007/9783662466698_6CrossRefGoogle Scholar
 21.Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: POPL, pp. 273–284. ACM (2008)Google Scholar
 22.Klensin, J.: Simple mail transfer protocol. RFC 5321, October 2008. https://tools.ietf.org/html/rfc5321
 23.Krcal, P., Yi, W.: Communicating timed automata: the more synchronous, the more difficult to verify. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 249–262. Springer, Heidelberg (2006). https://doi.org/10.1007/11817963_24CrossRefGoogle Scholar
 24.Laneve, C., Zavattaro, G.: Foundations of web transactions. In: Sassone, V. (ed.) FoSSaCS 2005. LNCS, vol. 3441, pp. 282–298. Springer, Heidelberg (2005). https://doi.org/10.1007/9783540319825_18CrossRefzbMATHGoogle Scholar
 25.Lapadula, A., Pugliese, R., Tiezzi, F.: CWS: a timed serviceoriented calculus. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 275–290. Springer, Heidelberg (2007). https://doi.org/10.1007/9783540752929_19CrossRefzbMATHGoogle Scholar
 26.Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Int. J. Softw. Tools Technolo. Transf. 1, 134–152 (1997)CrossRefGoogle Scholar
 27.López, H.A., Pérez, J.A.: Time and exceptional behavior in multiparty structured interactions. In: Carbone, M., Petit, J.M. (eds.) WSFM 2011. LNCS, vol. 7176, pp. 48–63. Springer, Heidelberg (2012). https://doi.org/10.1007/9783642298349_5CrossRefGoogle Scholar
 28.Milner, R.: Communicating and Mobile Systems: The \(\pi \)calculus. Cambridge University Press, New York (1999)zbMATHGoogle Scholar
 29.Murgia, M.: On urgency in asynchronous timed session types. In: ICE. EPTCS, vol. 279, pp. 85–94 (2018). https://doi.org/10.4204/EPTCS.279.9
 30.Neykova, R., Bocchi, L., Yoshida, N.: Timed runtime monitoring for multiparty conversations. Formal Asp. Comput. 29(5), 877–910 (2017). https://doi.org/10.1007/s0016501704208MathSciNetCrossRefzbMATHGoogle Scholar
 31.Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)zbMATHGoogle Scholar
 32.Saeedloei, N., Gupta, G.: Timed \(\pi \)calculus. In: Abadi, M., Lluch Lafuente, A. (eds.) TGC 2013. LNCS, vol. 8358, pp. 119–135. Springer, Cham (2014). https://doi.org/10.1007/9783319051192_8CrossRefGoogle Scholar
 33.Vinoski, S.: Advanced message queuing protocol. IEEE Internet Comput. 10(6), 87–89 (2006). https://doi.org/10.1109/MIC.2006.116CrossRefGoogle Scholar
 34.Yovine, S.: Kronos: a verification tool for realtime systems. (Kronos user’s manual release 2.2). Int. J. Softw. Tools Technol. Transf. 1, 123–133 (1997)CrossRefGoogle Scholar
Copyright information
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.