Timed Π-Calculus

We extend π -calculus with real-time by adding clocks and assigning time-stamps to actions. The resulting formalism, timed π -calculus, provides a simple and novel way to annotate transition rules of π -calculus with timing constraints. Timed π -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.