Timed $\pi$-Calculus

Abstract

We extend $\pi$-calculus with real-time by adding clocks and assigning time-stamps to actions. The resulting formalism, timed $\pi$-calculus, provides a simple and novel way to annotate transition rules of $\pi$-calculus with timing constraints. Timed $\pi$-calculus is an expressive way of describing mobile, concurrent, real-time systems in which the behavior of systems is modeled by finite or infinite sequences of timed events. We develop an operational semantics as well as a notion of timed bisimilarity for the proposed language. We present the properties of timed bisimilarity; in particular, expansion theorem for real-time, concurrent, mobile processes is investigated.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Introduction

The $\pi$-calculus was introduced by Milner et al. [12] with the aim of modeling concurrent/mobile processes. The $\pi$-calculus provides a conceptual framework for describing systems whose components interact with each other. It contains an algebraic language for describing processes in terms of the communication actions they can perform. Theoretically, the $\pi$-calculus can model mobility, concurrency and message exchange between processes as well as infinite computation (through the infinite replication operator ‘!’).

In many cases, processes run on controllers that control physical devices; therefore, they have to deal with physical quantities such as time, distance, pressure, acceleration, etc. Examples include communicating controller systems in cars (Anti-lock Brake System, Cruise Controllers, Collision Avoidance, etc.), automated manufacturing, smart homes, etc. Properties of such systems, which are termed cyber-physical systems (CPS) [6, 9], cannot be fully expressed within $\pi$-calculus. In a real-time/cyber-physical system the correctness of the system’s behavior depends not only on the tasks that the system is designed to perform, but also on the time instants at which these tasks are performed. While $\pi$-calculus can handle mobility and concurrency, it is not equipped to model real-time systems or CPS and support reasoning about their behavior related to time and other physical quantities. We extend $\pi$-calculus with real time so that these systems can be modeled and reasoned about.

Several extensions of $\pi$-calculus with time have been proposed [2, 4, 5, 10]; all these approaches discretize time rather than represent it faithfully as a continuous quantity. Discretizing means that time is represented through finite time intervals. As a result, infinitesimally small time intervals cannot be represented or reasoned about in these approaches. In practical real-time systems, e.g., a nuclear reactor, two or more events can occur within an infinitesimally small interval. Discretizing time can miss the modeling of such behavior which may be wholly contained within this infinitesimally small interval. In our approach for extending $\pi$-calculus with time, time is faithfully modeled as a continuous quantity. The most notable work on extending $\pi$-calculus with real time is the work of Chen [3]; however, the replication operator of the original $\pi$-calculus is not considered in this work. Therefore, it is unable to model infinite processes. In our approach the infinite behavior of timed precesses is modeled through the infinite replication operator ‘!’ as in original $\pi$-calculus.

We consider the extension of $\pi$-calculus with continuous time by adding finitely many real-valued clocks and assigning time-stamps to actions. The resulting formalism can be used for describing concurrent, mobile, real-time systems and CPS and reasoning about their behaviors.¹ In contrast to other extensions, in our work the notion of time and clocks is adopted directly from the well-understood formalism of timed automata [1]. For simplicity, the behavior of a real-time system is understood as a sequence (finite or infinite) of timed events, not states. The times of events are real numbers, which increase monotonically without bound.

Timed $\pi$-Calculus

Design Decisions

We define our timed $\pi$-calculus as an extension of the original $\pi$-calculus [12] with (local) clocks, clock operations and time-stamps. As in $\pi$-calculus, timed $\pi$-calculus processes use names (including clock names) to interact, and pass names to one another. These processes are identical to processes in $\pi$-calculus except that they have access to clocks which they can manipulate.

We assume an infinite set $\mathcal N$ of names (channel names and names passing through channels), an infinite set $\Gamma$ of clock names (disjoint from $\mathcal N$) and an infinite set $\varTheta$ of variables representing time-stamps (disjoint from $\mathcal{N}$ and $\Gamma$). When a process outputs a name through a channel, it also sends the time-stamp of the name and the clock that is used to generate the time-stamp. Inspired by the notion of name transmission in $\pi$-calculus, we can treat time-stamps and clocks just as other names and transmit them through/with channels. Just as channel transmission results in dynamic configuration of processes, clock and time-stamp transmission can result in dynamic temporal behavior of processes. Thus, messages are represented by triples of the form $\langle m,t_{m},c\rangle$, where $m$ is a name in $\mathcal N$, $t_m$ is the time-stamp on $m$, and $c$ is the clock that is used to generate $t_m$. It is important for the process to send its clock that is used to generate the time-stamp of the name, because the time-stamp of the incoming name in conjunction with the clock received is used by the receiving process to reason about timing requirements of the system as well as channel delays.

In our timed $\pi$-calculus all the clocks are local clocks; however, their scope is changed as they are sent among processes. This will become clear when we explain how clock passing is performed in Sect. 2.5. Keeping the clocks local results in a considerably simpler design of the timed $\pi$-calculus without sacrificing its practical applicability. Note that all the clocks advance at the same rate. A clock can be set to zero simultaneously with any transition (transitions are defined formally in Sect. 2.4). At any instant, the reading of a clock is equal to the time that has elapsed since the last time the clock was reset. Following the semantics of timed automata [1], we only consider non-Zeno behaviors, that is, only a finite number of transitions can happen within a finite amount of time.

Clock Operations and Clock Interpretations

We consider two types of clock operations: resetting a clock and checking satisfaction of a clock constraint. Resetting a clock is used to remember the time at which a particular action in the system has taken place. Clock resets are represented by $\gamma$ in the syntax of timed $\pi$-calculus. Clock constraints, denoted by $\delta$, indicate timing constraints between actions that occur in the system. Note that if $\delta$ contains more than one constraint, then the conjunction of all constraints must be considered. $\delta$ and $\gamma$ are defined by the following syntactic rules, in which $c$ and $c_i, 1\le i\le n$, are clock names, $r$ is a constant in $\mathbb {R}_{\ge 0}$, $t$ is a time-stamp and $\sim \in \{<,>,\le ,\ge ,=\}$. $\epsilon$ represents an empty clock constraint or clock reset.

$$\begin{aligned}&\delta \,{::=} (c \sim r)\delta ~\big | ~ (c - t \sim r)\delta ~\big | ~ (t - c \sim r)\delta ~ \big | ~\epsilon \\&\gamma \,{::=} (c_1:=0)\dots (c_n:=0)~ \big | ~\epsilon \end{aligned}$$

There are two ways to measure the passing of time while checking for a clock constraint. It can be measured and reasoned about against (i) the last time a clock was reset: e.g., a constraint $(c < 2)$ on sending $m$ indicates that $m$ must be sent out within two units of time since the clock $c$ was reset, or (ii) the last time a clock $c$ was reset in conjunction with a time-stamp $t$ of a name. Note that in this case, the time-stamp $t$ must be generated by clock $c$. For instance, suppose that a process $P$ sends two consecutive names that are two units of time apart; if the time-stamp of the first name, generated by clock $c$ is $t_{1}$, then the expression $c-t_{1}=2$ can be used to express this constraint.

For a process $P$, we define $c(P)$ to be the set of clock names in $P$. For every two processes $P$ and $Q$ we assume $c(P)\cap c(Q)=\emptyset$, initially. This property is also maintained all the time as transitions take place. A clock interpretation $I$ for a set $\Gamma$ of clocks is a mapping from $\Gamma$ to $\mathbb {R}_{\ge 0}$. It assigns a real value to each clock in $\Gamma$. A clock interpretation $I$ for $\Gamma$ satisfies a clock constraint $\delta$ over $\Gamma$ iff the expression obtained by applying $I$ to $\delta$ evaluates to true. For $t \in \mathbb {R}_{\ge 0}$, $I+t$ denotes the clock interpretation which maps every clock $c$ to the value $I(c)+t$. For $\gamma \subseteq \Gamma$, $[\gamma \mapsto t]I$ denotes the clock interpretation for $\Gamma$ which assigns $t$ to each $c \in \gamma$, and agrees with $I$ over the rest of the clocks.

Syntax

The set of timed $\pi$-calculus processes is defined by the following syntactic rules in which, $P$, $P^\prime$, $M$ and $M^\prime$ range over processes, $x,y$ and $z$ range over names in $\mathcal N$, $c$ and $d$ range over clock names in $\Gamma$, and $t_y$ represents a time-stamp.

$$\begin{aligned} M&{::=} \delta \gamma \bar{x}\langle y, t_{y}, c \rangle .P ~ \big | ~\delta \gamma x(\langle y, t_{y}, c \rangle ).P ~ \big | ~ \delta \gamma \tau .P~\big |~ 0~\big | ~M+M^\prime \\ P&{::=} M~\big |~(P ~ | ~ P^\prime )~ \big | ~ !P ~\big | ~ (z) ~ P~\big | ~ \left[ x = y \right] P ~\big | ~ \left[ c = d \right] P \end{aligned}$$

The expression $\delta \gamma \bar{x}\langle y, t_{y}, c \rangle .P$ represents a process that is capable of outputting name $y$ on channel $x$. This process generates a time-stamp $t_y$ using clock $c$ and sends $t_y$ and $c$ along with $y$ via the channel $x$, and evolves to $P$. The time-stamp $t_y$ is the reading of clock $c$ at the time of transition. The assignment of a time-stamp to $y$ and sending $y$ is an atomic operation. The clock constraint $\delta$ must be satisfied by the current value of clocks at the time of transition. $\gamma$ specifies the clocks to be reset with this transition.

Example 1

The process $P=(c<2)\bar{x}\langle y,t_{y},c \rangle .P'$ is capable of sending name $y$ on channel $x$ within two units of time since clock $c$ was last reset. Note that the time-stamp of $y$ is the reading of clock $c$ when the output takes place. Since the output can happen only within two units of time since $c$ was last reset, then time-stamp $t_y$ is a positive real number less than two ($t_y<2$). $t_y$ and $c$ are both sent along with $y$ through channel $x$.

The expression $\delta \gamma x(\langle y, t_{y}, c \rangle ).P$ stands for a process which is waiting for a message on channel $x$. When a message arrives, the process will behave like $P\{z/y, t_z/t_y, d/c\}$ (substitution is formally defined in Definition 2) where $z$ is the name received; $t_z$ is the time-stamp of $z$; and $d$ is the clock of the sending process that is used to generate $t_z$. The time-stamp $t_z$ must satisfy the clock constraint expressed by $\delta$; $\gamma$ specifies the clocks to be reset with the transition.

Example 2

Assume process $Q=(e>5)(d-{t_z}\le 3)x(\langle z,t_{z},d \rangle ).Q'$ is the receiving process in Example 1. The received name, along with its time-stamp and the accompanying clock will be substituted for $z$, $t_z$ and $d$, respectively. After substitution takes place, the constraint $c-{t_y}\le 3$ specifies how long the received name was on transit. Any delay greater than three is not acceptable and cause the input action to not take place. Note that $e$ is another local clock of $Q$. Both constraints $e>5$ and $(d-{t_z}\le 3)$ must be satisfied by the current value of clocks for the input action to take place.

Note that time-stamps are put on names only by the sending processes, that is no time-stamps are assigned to received names upon arrival. The value of a time-stamp generated by process $P$ on sending name $y$, is the value of $P$’s local clock $c$ at the time of output. This value is generated such that it satisfies the clock constraint corresponding to the output action. Note that in Example 2, $t_z$ gets bound to the time-stamp of the incoming name, as we do not assign time-stamps to the received names.

The expression $\delta \gamma \tau .P$ stands for a process that takes an internal action and evolves to $P$, and in doing so resets the clocks specified by $\gamma$, if the clock constraint $\delta$ is satisfied.

In each of three processes explained above, if the clock constraint $\delta$ is not satisfied by the value of clocks at the time of transition, then, the process becomes inactive. An inactive process, represented by $0$, is a process that does nothing.

The operators $+$ and $|$ are used for nondeterministic choice and composition of processes, just as in $\pi$-calculus [12]. The replication $!P$, represents an infinite composition $P~|~P~|\dots$, just as in $\pi$-calculus. The restriction $(z)P, z \in \mathcal N$, behaves as $P$ with $z$ local to $P$. Therefore, $z$ cannot be used as a channel over which to communicate with other processes or the environment. $\left[ x = y \right] P, x,y\in \mathcal{N}\cup \Gamma$, evolves to $P$ if $x$ and $y$ are the same name; otherwise, it becomes inactive.

Example 3

The timed $\pi$-calculus expression $x(\langle m,t_m,c \rangle ).(c-t_m\le 5)\bar{y}\langle n,t_n,c\rangle$ represents a process that is waiting for a message on channel $x$. The process upon receiving a name $m$ with time-stamp $t_m$ and its accompanying clock $c$ on channel $x$, sends a name $n$ with time-stamp $t_{n}$ on channel $y$ with the delay of at most 5 units of time since the time-stamp of $m$. The process will use the clock $c$ to choose a time $t_{n}$ on $c$ such that $c-t_{m}\le 5$.

In a process of the form $\delta \gamma x(\langle y,t,c\rangle ).P$ the occurrences of $y$, $t$ and $c$ are binding occurrences, and the scope of the occurrences is $P$. In $(n)P, n\in \mathcal{N}$ the occurrence of $n$ is a binding occurrence, and the scope of the occurrence is $P$.

Definition 1

An occurrence of a (non-clock) name $n$ in a process is free if it does not lie within the scope of a binding occurrence of $n$. An occurrence of a (non-clock) name in a process is bound if it is not free. All occurrences of a clock $c$ in a process $P$ are bound. The set of bound names of $P$, $bn(P)$, contains all names which occur bound in $P$. The set of names occurring free in $P$ is denoted $fn(P)$. We write $n(P)$ for the set $fn(P) \cup bn(P)$ of names of $P$.

Intuitively, the free (non-clock) names of a process, represent its (public) links to other processes. For instance, if processes $P$ and $Q$ share the same free name $x$, then, the channel $x$ is shared between these two processes.

Example 4

Let $P = x(\langle y,t,c\rangle ).0$ and $Q = (d>1)(d<5)\bar{x}\langle z,t^\prime ,d\rangle .0$. Then, $fn(P)=\{x\}, bn(P)=\{y,t,c\}$, $fn(Q)=\{x,z,t'\}$, and $bn(Q)=\{d\}$. $x$ is a channel that is shared between $P$ and $Q$. This behavior can be represented for example in the parallel composition of $P$ and $Q$: $(P~|~Q)$.

Definition 2

[12] A substitution is a function $\theta$ from a set of names $\mathcal N$ to $\mathcal N$. If $x_i\theta =y_i$ for all $i$ with $1 \le i \le n$ (and $x\theta =x$ for all other names $x$), we write $\{y_1/x_1,\dots ,y_n/x_n\}$ for $\theta$.

The effect of applying a substitution $\theta$ to a process $P$ is to replace each free occurrence of each name $x$ in $P$ by $x\theta$, with change of bound names to avoid name capture (to preserve the distinction of bound names from the free names). Substitution for time-stamps can be defined similarly.

Definition 3

A clock substitution is a function ${\theta }_c$ from a set of clock names $\Gamma$ to $\Gamma$. If $c_i{\theta }_c=d_i$ for all $i$ with $1 \le i \le n$ (and $c{\theta }_c=c$ for all other clock names $c$), we write $\{d_1/c_1,\dots ,d_n/c_n\}$ for ${\theta }_c$.

The effect of applying a substitution ${\theta }_c$ to a process $P$, $P{\theta _c}$, is to replace all occurrences of each clock name $c$ in $P$ by $c{\theta }_c$.

Definition 4

Given a clock $c$, the function ${\theta _f}$ creates a fresh copy, $f$, of $c$ ($f$ does not appear in any process) and updates the interpretation with $I(f)=I(c)$. The application of $\theta _f$ to $c$ is represented by $c{\theta _f}$.

Definition 5

A clock renaming ${\theta }_r$ is a clock substitution $\{f_1/c_1,\dots ,f_n/c_n\}$ in which $f_i = c_i{\theta _f}, 1 \le i \le n$.

The effect of applying a clock renaming ${\theta }_r=\{f_1/c_1,\dots ,f_n/c_n\}$ to process $P$, $P{\theta _r}$, is to replace all occurrences of each name $c$ in $P$ by $c{\theta }_r$.

Operational Semantics

First, we define actions by the following syntactic rule:

$$\begin{aligned} \alpha {::=} \bar{x}\langle y, t, c \rangle ~ \big | ~ \bar{x}\langle (y), t, c \rangle ~ \big | x(\langle y, t, c \rangle ) ~ \big |~ \tau \end{aligned}$$

The first two actions are the bound output actions. Bound output actions are used to carry names out of their scope. $\bar{x}\langle y, t, c \rangle$ is used for sending a name $y$, time-stamp of $y$, $t$, and the (local) clock that is used to generate $t$, via channel $x$. The process that gives rise to this action can be of the form $\bar{x}\langle y,t,d \rangle .P, c=d{\theta _f}$. In this action $x$, $y$ and $t$ are free and $c$ is bound; $c$ is the fresh copy of $d$. The expression $\bar{x}\langle (y), t, c \rangle$ is used by a process for sending its private name $y$ ($y$ is bound in the process) and its (local) clock $c$. The process that gives rise to this action can be of the form: $(y)\bar{x}\langle y,t,d \rangle .P, c=d{\theta _f}$. In this action $x$ and $t$ are free, while $y$ and $c$ are bound²; $c$ is a fresh copy of $d$.

As we mentioned before all the clocks in the calculus are local clocks: the clocks of a process $P$ are accessible only by $P$. However, the scope of the clocks is extended as they are sent to other processes. If $d$ is sent to process $Q$ by $P$, then both $P$ and $Q$ will have access to $d$. As a result, they both can reset $d$ as part of their future transitions. To prevent processes interfering with each other by resetting a shared clock, $P$ must create a fresh copy of $d$, let us call it $c$, and send $c$ to $Q$. This is the reason of creating fresh copies of clocks in both output actions.

Table 1. Timed $\pi$-calculus transition rules

The third action is the input action $x(\langle y, t, c \rangle )$. This action is used for receiving any name $z$ with its time-stamp $t_z$, and a clock $d$ via $x$. $y$, $t$ and $c$ are place holders in the receiving process for values that will be received as inputs. In this action $x$ is free, while $y, t$ and $c$ are bound names.

The last action is the silent action $\tau$, which is used to express performing an internal action. Silent actions can naturally arise from processes of the form $\tau .P$, or from communications within a process (e.g., rule COM in Table 1).

We use $fn(\alpha )$ for set of free names of $\alpha$, $bn(\alpha )$ for set of bound names of $\alpha$, and $n(\alpha )$ for the union of $fn(\alpha )$ and $bn(\alpha )$. Note that $fn(\tau )=\emptyset$ and $bn(\tau )=\emptyset$.

A transition in timed $\pi$-calculus is of the form $P\xrightarrow {\langle \delta , \alpha , \gamma \rangle }P^\prime$. This transition is understood as follows: if $\delta$ is satisfied by the current values of clocks, $P$ evolves into $P^\prime$, and in doing so performs the action $\alpha$ and resets the clocks specified by $\gamma$. With abuse of notation, we have used $\gamma$ as a set of clocks to be reset. We call the triple $\langle \delta , \alpha , \gamma \rangle$ a timed action. The set of transition rules of timed $\pi$-calculus are represented in Table 1. These rules are labeled by timed actions.

In rule IN the incoming clock and time-stamp must satisfy the clock constraint in the receiving process, for transition to take place. The incoming clock might get reset upon arrival in the receiving process. These requirements are specified in the timed action for IN where $t'$ and $d$ (the received time-stamp and clock) are substituted for $t$ and $c$, respectively. In rule OUT, $d$ is a fresh copy of clock $c$ which is created and sent along name $y$ on outputting the name. The rule for COM is similar to that of original $\pi$-calculus; however, the clock $c$ communicated between $P$ and $Q$ is a fresh clock name generated by rule OUT (the premise of COM).

The joint use of two rules OPEN and CLOSE is used for scope-extrusion of bound names (including clock names). A bound output combines with an input action, and once the bound name has been received, a restriction will be extended to the receiving process. This means the received name is still bound although its scope has grown. However, this restriction should not bind occurrences of free names in the receiving process. This is the reason for changing the name $y$ to a fresh name $u$ before sending $y$, as in the original $\pi$-calculus. Note that the OPEN rule does not changes the clock name $c$, as $c$ is a fresh clock name generated by the rule OUT (the premise of OPEN).

Note that in the rule for REP the set of clock names in $P'$ are replaced by fresh clock names by applying the renaming ${\theta }_r$ to $P'$. Similarly, in the rules for REP-COM and REP-CLOSE the clock names in the replicated processes are replaced by fresh clock names using ${\theta '}_r$ and ${\theta ''}_r$. Note also that there are two more rules for SUM and PAR where the process $Q$ takes an action. These rules are symmetric to SUM and PAR rules of Table 1 and are eliminated.

Example 5

Using OUT and OPEN we can derive:

$$\begin{aligned} (y)\bar{x}\langle y,t, c\rangle .P\xrightarrow {\langle \epsilon ,\bar{x}\langle (u), t, d \rangle , \epsilon \rangle }P\{u/y\} \end{aligned}$$

For all $u$ such that $u$ is $y$ or $u\notin fn(P)$ and $d=c{\theta _f}$. Using IN we have that

$$\begin{aligned} x(\langle z,t_z,e\rangle ).Q\xrightarrow {\langle \epsilon ,x(\langle u, t, d \rangle ), \epsilon \rangle }Q\{u/z,t/t_z,d/e\} \end{aligned}$$

For all $u$ such that $u$ is $z$ or $u\notin fn(Q)$. By applying CLOSE we derive

$$\begin{aligned} ((y)\bar{x}\langle y,t, c\rangle .P~|~x(\langle z,t_z,e\rangle ).Q)\xrightarrow {\langle \epsilon , \tau , \epsilon \rangle }(u)(P\{u/y\}~ |~ Q\{u/z,t/t_z,d/e\}) \end{aligned}$$

Next, we formally define the operational semantics of timed $\pi$-calculus and how the transitions change the interpretation.

Definition 6

[1] A time sequence $w=w_1w_2\dots$ is a finite or infinite sequence of time values $w_i\in \mathbb {R}$ with $w_i>0$, satisfying the following constraints:

• Monotonicity: $w$ increases strictly monotonically; that is, $w_i<w_{i+1}$ for all $i\ge 1$.

• Progress: For every $w\in \mathbb {R}$, there is some $i\ge 1$ such that $w_i\ge w$.

A system specified by set of timed $\pi$-calculus processes starts with all the clocks initialized to 0. Moreover, for every two processes $P$ and $Q$, $c(P)\cap c(Q) = \emptyset$, initially. As time advances the value of all clocks advances, reflecting the elapsed time. At time $w_i$, a process $P_{i-1}$ takes a timed action $\langle \delta _i, \alpha _i, \gamma _i \rangle$ and evolves to $P_i$, if the current values of clocks satisfy $\delta _i$. The clocks specified by $\gamma _i$ are reset to 0, and thus start counting time with respect to it. This behavior is captured by defining runs of timed $\pi$-calculus processes. A run for a process $P$, records the state (process expression) and the values of all the clocks at the transition points. For a time sequence $w=w_1w_2\dots$ we define $w_0=0$.

Definition 7

A run $r$, denoted by $(\bar{P}, \bar{I})$, of a timed $\pi$-calculus process $P$, is a finite or an infinite sequence of the form

$$\begin{aligned} \langle P_0, I_0 \rangle \xrightarrow [w_1]{\langle \delta _1, \alpha _1, \gamma _1 \rangle } \langle P_1, I_1 \rangle \xrightarrow [w_2]{\langle \delta _2, \alpha _2, \gamma _2 \rangle } \langle P_2, I_2 \rangle \xrightarrow [w_3]{\langle \delta _3, \alpha _3, \gamma _3 \rangle } \dots \end{aligned}$$

where $P_i$ is a process and $I_i\in [\Gamma \rightarrow \mathbb {R}_{\ge 0}]$, for all $i\ge 0$, satisfying the following requirements:

• Initiation: $P_0$ is the initial process expression, and $I_0(c)=0$ for all $c\in \Gamma$.

• Consecution: for all $i\ge 1$, there is a transition of the form $P_{i-1} \xrightarrow {\langle \delta _i, \alpha _i, \gamma _i \rangle }P_i$ such that $(I_{i-1}+w_i-w_{i-1})$ satisfies $\delta _i$ and $I_i=[\lambda _i\mapsto 0](I_{i-1}+w_i-w_{i-1})$.

Along a run $r=(\bar{P}, \bar{I})$, the values of the clocks at time $w_i\le w\le w_{i+1}$ are given by the interpretation $(I_i+w-w_i)$. When the transition from $P_i$ to $P_{i+1}$ occurs, the value $(I_i+w_{i+1}-w_i)$ is used to check the clock constraint. At time $w_{i+1}$, the value of a clock that gets reset is defined to be 0.

When the transition from $P_i = \delta \gamma x(\langle z,t,c\rangle ).P$ to $P_{i+1} = P\{y/z,t'/t,d/c\}$ occurs ($\langle y,t',d\rangle$ is the received name), we check the satisfiability of the clock constraint $\delta \{d/c,t'/t\}$, similarly we reset the clocks specified by $\gamma \{d/c\}$. Intuitively, this means that the values of the received clock and time-stamp should satisfy the constraint $\delta$ for the transition to take place. Moreover, the incoming clock might get reset upon arrival. These requirements are specified in the timed action of rule IN in Table 1. When the transition from $P_i = \delta \gamma \bar{x}\langle y, t, c \rangle .P$ to $P_{i+1} = P$ occurs in which, the timed action $\langle \delta ,\bar{x}\langle y, t, d \rangle , \gamma \rangle , d=c{\theta _f}$ takes place, the time-stamp $t$ in $\bar{x}\langle y, t, d \rangle$ gets bound to $(I_{i}(c)+w_{i+1}-w_i)$. Note that at this point $I_{i+1}(d)=I_{i+1}(c)$.

Passing Clocks and Channels

Link (channel) passing in timed $\pi$-calculus is handled in exactly the same manner as in $\pi$ calculus, in the sense that a process $P$ can send a public channel $x$ to a process $Q$. However, if $Q$ already has access to a private channel $x$ before the transition, the latter must be renamed to avoid confusion: this is called scope intrusion [12]. If $P$ has a private link $x$ that it sends to $Q$, the scope of restriction will be extended, this is called scope extrusion [12]. In this case, if $Q$ already has access to a public link $x$, then the name of the private link must be changed before the transition (these are reflected in rules OPEN and CLOSE).

All clocks in timed $\pi$-calculus are local clocks; moreover, processes access disjoint sets of clocks. When a process $P$ sends its (local) clock $c$ to another process $Q$, it creates a fresh copy of $c$ and sends this copy to $Q$.

Assume that $P = \delta \gamma \bar{y}\langle x,t_x,c\rangle .P^\prime$ and $Q = \delta ^\prime \gamma ^\prime y(\langle z,t_z,d\rangle ).Q^\prime$. Furthermore, assume that $P$ sends $\langle x,t_x,c\rangle$ to process $Q$. This behavior can be captured by the following timed $\pi$-calculus transition.

$$\begin{aligned} (P ~ \big | ~ Q) \xrightarrow {\langle \delta \delta ^\prime , \tau , \gamma \gamma ^\prime \rangle } (P^\prime ~ |~ Q^\prime \{x/z, t_x/t_z, e/d\}), ~~~~~e=c{\theta _f} \end{aligned}$$

Next, we define the structural congruence for proposed timed $\pi$-calculus.

Structural Congruence

The notion of structural congruence for timed $\pi$-calculus processes is identical to that of original $\pi$-calculus [12]. Two timed $\pi$-calculus processes are structurally congruent if they are identical up to structure. Structural congruence, $\equiv$, is the least equivalence relation preserved by the process constructs that satisfy the axioms in Table 2.

Table 2. Axioms of structural congruence

Timed Bisimulation

We would like to identify two processes which cannot be distinguished by an observer. We assume that the observer is able to observe all kinds of actions and moreover, it can observe the times at which the actions are taken place.

Definition 8

A binary relation $\mathcal S$ on timed $\pi$-calculus processes is a (strong) timed simulation if $P\mathcal{S}Q$ implies that:

• 1. If $\langle P, I \rangle \xrightarrow [w]{\langle \delta , \tau , \gamma \rangle } \langle P', I' \rangle$, then for some $Q^\prime$, $\langle Q, I \rangle \xrightarrow [w]{\langle \delta , \tau , \gamma \rangle } \langle Q', I' \rangle$ and $P^\prime \mathrel {\mathcal {S}} Q^\prime$,

• 2. If $\langle P, I \rangle \xrightarrow [w]{\langle \delta , \bar{x}\langle y, t, c \rangle , \gamma \rangle } \langle P', I' \rangle$, then for some $Q^\prime$, $\langle Q, I \rangle \xrightarrow [w]{\langle \delta , \bar{x}\langle y, t, c \rangle , \gamma \rangle } \langle Q', I' \rangle$ and $P^\prime \mathrel {\mathcal {S}} Q^\prime$,

• 3. If $\langle P, I \rangle \xrightarrow [w]{\langle \delta , \bar{x}\langle (y), t, c \rangle , \gamma \rangle } \langle P', I' \rangle$ and $y \notin n(P,Q)$, then for some $Q^\prime$, $\langle Q, I \rangle \xrightarrow [w]{\langle \delta , \bar{x}\langle (y), t, c \rangle , \gamma \rangle } \langle Q', I' \rangle$ and $P^\prime \mathrel {\mathcal {S}} Q^\prime$,

• 4. If $\langle P, I \rangle \xrightarrow [w]{\langle \delta , x(\langle y, t, c \rangle ), \gamma \rangle } \langle P', I' \rangle$ and $y \notin n(P,Q)$, then for some $Q^\prime$, $\langle Q, I \rangle \xrightarrow [w]{\langle \delta , x(\langle y, t, c \rangle ), \gamma \rangle } \langle Q', I' \rangle$ and for all $z$, $P^\prime \{z/y\}\mathrel {\mathcal {S}} Q^\prime \{z/y\}$.

The relation $\mathcal S$ is a (strong) timed bisimulation if both $\mathcal S$ and its inverse are timed simulation. The relation $\dot{\sim }$, (strong) bisimilarity, on timed processes is defined by $P \dot{\sim } Q$ if and only if there exists a timed bisimulation $\mathcal S$ such that $P \mathcal S$ $Q$.

Example 6

Assume $P$ is a timed $\pi$-calculus process defined as:

$$\begin{aligned} (c<2)(c:=0)\bar{x}\langle y,t_y,c\rangle ~|~(d:=0)z(\langle w,t_w,d\rangle ) \end{aligned}$$

in which, $x\ne z$. Then,

$$\begin{aligned} P ~&\dot{\sim }~ (c<2)(c:=0)\bar{x}\langle y,t_y,c\rangle .(d:=0)z(\langle w,t_w,d\rangle ) + \\ ~~~~~~&~~~(d:=0)z(\langle w,t_w,d\rangle ).(c<2)(c:=0)\bar{x}\langle y,t_y,c\rangle \end{aligned}$$

Analogous to strong bisimilarity in $\pi$-calculus, $\dot{\sim }$ is not in general preserved by substitution of names. It follows that (strong) timed bisimilarity is not preserved by input prefix. As a result, (strong) timed bisimilarity is not a congruence.

Example 7

Assume $P$ is defined as in Example 6, and $Q=u(\langle z,t_z,e\rangle ).(P)$ Then,

$$\begin{aligned} Q ~&\dot{\not \sim }~u(\langle z,t_z,e\rangle ).((c<2)(c:=0)\bar{x}\langle y,t_y,c\rangle .(d:=0)z(\langle w,t_w,d\rangle ) +\\&~~~~~~~~~~~~~~~~~~~~~~~~~(d:=0)z(\langle w,t_w,d\rangle ).(c<2)(c:=0)\bar{x}\langle y,t_y,c\rangle ) \end{aligned}$$

The reason is that, if $z$ is instantiated to $x$ (the channel name received in $u$ is $x$), then $P\{x/z\}$ will have a $\tau$ transition which cannot be simulated by the right hand side of the equation.

Definition 9

If $x \ne y$, then $\delta \gamma \bar{x}\langle (y),t,c\rangle .P$ means $(y)~\delta \gamma \bar{x}\langle y,t,c\rangle .P$, and the prefix $\bar{x}\langle (y),t,c\rangle$ is called a derived prefix.

A collection of algebraic laws for (strong) timed bisimilarity, which are extensions of algebraic laws for bisimilarity in $\pi$-calculus [12], is presented in Table 3. Note that $\rho$ in proposition 5(d) denotes a prefix, including a derived prefix.

Table 3. Timed bisimilarity algebraic laws

Proposition 7 Expansion

Let $P \equiv \sum _{i} \delta _{i}\gamma _{i}\rho _i.P_i$ and $Q \equiv \sum _{j} \eta _{j}\lambda _{j}\phi _j.Q_j$ where $\delta _i$ and $\eta _j$ are constraints, $\gamma _i$ and $\lambda _j$ specify the set of clocks to be reset and $\rho _i$ and $\phi _j$ are prefixes; $bn(\rho _i) \cap fn(Q) = \emptyset$ for all $i$, and $bn(\phi _j) \cap fn(P) = \emptyset$ for all $j$; then

$$\begin{aligned}&\qquad \quad P~|~Q ~\dot{\sim } ~\sum _{i} \delta _{i}\gamma _{i}\rho _i.(P_i~ |~ Q)+\\&\sum _{j} \eta _{j}\lambda _{j}\phi _j.(P~ |~ Q_j)+ \sum _{\rho _i \text {comp} \phi _j} \delta _{i}\eta _{j}\gamma _{i}\lambda _{j}\tau .R_{ij} \end{aligned}$$

The relation $\rho _i$ comp $\phi _j$ ($\rho _i$ complements $\phi _j$) holds in the following four cases, which also defines $R_{ij}$:

• 1. $\rho _i$ is $\bar{x}\langle u,t,c\rangle$ and $\phi _j$ is $x(\langle v,t_v,d\rangle )$; then $R_{ij}$ is $(P_i | Q_j\{u/v,t/t_v,e/d\})$ where $e=c{\theta _f}$,

• 2. $\rho _i$ is $\bar{x}\langle (u),t,c\rangle$ and $\phi _j$ is $x(\langle v,t_v,d\rangle )$; then $R_{ij}$ is $(w)(P_i\{w/u\} | Q_j\{w/v,t/t_v,e/d\})$ where $w$ is not free in $(u)P_i$ or in $(v)Q_j$ and $e=c{\theta _f}$,

• 3. $\rho _i$ is $x(\langle v,t_v,d\rangle )$ and $\phi _j$ is $\bar{x}\langle u,t,c\rangle$; then $R_{ij}$ is $(P_i\{u/v,t/t_v,e/d\} | Q_j)$ where $e=c{\theta _f}$,

• 4. $\rho _i$ is $x(\langle v,t_v,d\rangle )$ and $\phi _j$ is $\bar{x}\langle (u),t,c\rangle$; then $R_{ij}$ is $(w)(P_i\{w/v,t/t_v,e/d\} | Q_j\{w/u\})$ where $w$ is not free in $(v)P_i$ or in $(u)Q_j$ and $e=c{\theta _f}$.

Proofs of above propositions are extensions of the proofs for untimed $\pi$-calculus processes [12] (these extensions take clocks into account) which are not presented here due to lack of space.

Example: The Railroad Crossing Problem

The generalized railroad crossing (GRC) problem [7] describes a railroad crossing system with several tracks and an unspecified number of trains traveling through the tracks. The gate at the railroad crossing should be operated in a way that guarantees the safety and utility properties. The safety property stipulates that the gate must be down while there is a train in the crossing. The utility property states that the gate must be up (or going up) when there is no train in the crossing. The system is composed of three components: train, controller and gate. The components of the system which are specified via three timed automata in Fig. 1, communicate by sending and receiving signals. We specify the components of the system in timed $\pi$-calculus.

Fig. 1.

Timed automata for train, controller, and gate in the railroad crossing problem

The controller at the railroad crossing might receive various signals from trains in different tracks. In order to avoid signals from different trains being mixed, each train communicates through a private channel with the controller. A new channel is established for each approaching train to the crossing area through which the communication between the train and the controller takes place. For simplicity of presentation we consider only one track in this example.

Table 4. The timed $\pi$-calculus expressions for components of the railroad crossing problem)

In our modeling of railroad crossing problem in timed $\pi$-calculus each component of the system is considered as a timed $\pi$-calculus process. This model is presented in Table 4. Note that the design of the railroad crossing problem shown in Fig. 1 (originally from [1]) does not account for the delay between the sending of approach (exit) signal by a train and receiving it by the controller. Similarly the delay between sending lower (raise) by the controller and receiving it by the gate is not taken into account. Arguably, in a correct design, the delay before approach is received by the controller should be taken into account. The lower signal must be sent within one unit of time since the time-stamp of the original approach but not the time at which the controller receives the signal (note that the controller resets its clock to remember the time it receives approach). In contrast, in our specification of the railroad crossing problem in timed $\pi$-calculus, we are considering the delays; therefore, all the time-related reasoning in the system is performed against train’s clock and the time-stamp of approach signal (sent by train to controller).

Note that in the $\pi$-calculus expression for train specified in Table 3, $t$ is the local clock of train and the two consecutive $\tau$ actions correspond to train’s internal actions in and out. In the expression for controller, $c$ is a place holder for the received clock $t$ from train; while, $e$ is the controller’s clock that is reset before it is sent to gate. In the expression for gate, $g$ is a place holder for the received clock $e$ from controller and the two $\tau$ actions correspond to gate’s internal actions; the first $\tau$ represents down; while the second $\tau$ represents up.

Timed $\pi$-calculus allows the railroad crossing problem to be modeled more faithfully. Additionally, significantly more complex systems can be modeled. The timed $\pi$-calculus specification can be used for verification of the system as well as generating the implementation [15].

Discussions

Our proposed timed $\pi$-calculus extends the original $\pi$-calculus of Milner, while preserving the algebraic properties of the original $\pi$-calculus. The notion of timed bisimilarity and expansion in our calculus are also simple extensions of those found in the original $\pi$-calculus. Our calculus is a simple and powerful calculus which annotates the transitions of $\pi$-calculus with timing constraints. Our effort was driven by our desire to keep the design simple. The two most critical and fundamental assumptions/decisions made in this paper are discussed next.

First, on outputting a name we submit a clock and also the time-stamp of the name generated by the clock. Without time-stamps, precisely reasoning about channel delays becomes much more complex, if not impossible. As an example consider a scenario in which process $P$ takes an action $\alpha$ and resets its clock $c$ at the time of action in order to remember when the action took place. Let us assume that after $t$ units of time ($t$ is measured by $c$) have elapsed since $\alpha$’s occurrence, $P$ sends a name $n$ (along with clock $c$ and time-stamp $t_n$ generated by $c$) to process $Q$. Note that $P$ did not reset the clock before this output, as it continues to need to measure the time since the occurrence of $\alpha$. At this point if we wanted to know for how long the name $n$ was in transit, we could not calculate it without $t_n$. However, on receiving $n$ on $Q$, the expression $c-t_n$ could be used to calculate the exact time for which the name $n$ was in transit.

The second fundamental design decision in our calculus is our choice of local clocks and how clocks are treated. Initially, processes have access to distinct set of clocks. Later, after transitions take place, the scope of local clocks may grow; however, we keep the distinction between clocks of different processes. We achieve this by having processes create fresh copies of their own clocks (and updating the interpretation accordingly) and sending these copies instead of their original clocks. Adopting this convention prevents processes from resetting each others’ clocks, as the sending process may keep using (possibly resetting) the clock that was sent for measuring other subsequent events. Our choice of clocks and our careful treatment of clocks enabled us to extend the transition rules of the original $\pi$-calculus naturally in order to obtain the transition rules of our timed $\pi$ calculus. It also made our expansion theorem an straightforward extension of the original one.

Conclusions and Related Work

Since the $\pi$-calculus was proposed by Milner et al. [12], many researchers have extended it for modeling distributed real-time systems. Berger has introduced timed $\pi$-calculus ($\pi _{t}$-calculus) [2], asynchronous $\pi$-calculus with timers and a notion of discrete time, locations, and message failure, and explored some of its basic properties. Olarte has studied temporal CCP (tcc) as a model of concurrency for mobile, timed reactive systems in his Ph.D thesis [13]. He has developed a process calculus called universal temporal CCP (utcc). His work can be seen as adding mobile operation to the tcc. In utcc, like tcc, time is conceptually divided into time intervals (or time units); therefore it is discretized. Lee et al. [10] introduced another timed extension of $\pi$-calculus called real-time $\pi$-calculus ($\pi$RT-calculus). They have introduced the time-out operator and considered a global clock, single observer as part of their design, as is common in other (static) real-time process algebras. They have used the set of natural numbers as the time domain, i.e., time is discrete and is strictly increasing. Ciobanu et al. [4] have introduced a model called timed distributed $\pi$-calculus in which they have considered timers for channels, by which they restrict access to channels. They use decreasing timers, and time is discretized in their approach also. Many other timed calculi have similar constructs which also discretize time [5, 8, 11]. In summary, all these approaches share some common features; they use a discrete time-stepping function or timers to increase/decrease the time-stamps after every action (they assume that every action takes exactly one unit of time). In contrast, our approach for extending $\pi$-calculus with time faithfully treats time as continuous.

Posse et al. [14] have proposed $\pi _{klt}$-calculus as a real-time extension of $\pi$-calculus and study a notion of time-bounded equivalence. They have developed an abstract machine for the calculus and developed an implementation based on this abstract machine for the $\pi _{klt}$-calculus in a language called kiltera. The replication operator of the original $\pi$-calculus is missing in this work.

The work of Yi [17] shows how to introduce time into Milner’s CCS to model real-time systems. An extra variable $t$ is introduced which records the time delay before a message on some channel $\alpha$ is available, and also a timer for calculating delays. The idea is to use delay operators to suspend activities. In our opinion, it is much harder to specify real-time systems using delays. Our approach provides a more direct way of modeling time in $\pi$-calculus via clocks, and also can be used to elegantly reason about delays.

The proposed timed $\pi$-calculus is an expressive, natural model for describing real-time, mobile, concurrent processes. It preserves the algebraic rules of the original $\pi$-calculus, while keeps the expansion theorem simple.

With respect to future work, we would like to extend our timed $\pi$-calculus with other continuous quantities; so that more complex systems as well as CPS can be expressed. While we have used our calculus for modeling and verifying the railroad crossing problem [15], we would like to model the generalized railroad crossing (GRC) problem in our calculus and use it for verifying properties of the system.