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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
While we only focus on extending the \(\pi \)-calculus with continuous time, our method serves as a model for extending the \(\pi \)-calculus with other continuous quantities. An instance of this, though not in the context of \(\pi \)-calculus, can be found in [16].
- 2.
Since all the clocks are local clocks and all clock names are bound, we do not use parenthesis as we do for regular names to distinguish them from free names.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Berger, M.: Towards abstractions for distributed systems. Technical report, Imperial College London (2004)
Chen, J.: Timed extensions of \(\pi \) calculus. Theor. Comput. Sci. 11(1), 23–58 (2006)
Ciobanu, G., Prisacariu, C.: Timers for distributed systems. Electr. Notes Theor. Comput. Sci. 164(3), 81–99 (2006)
Degano, P., Loddo, J.V., Priami, C.: Mobile processes with local clocks. In: Dam, M. (ed.) LOMAPS-WS 1996. LNCS, vol. 1192, pp. 296–319. Springer, Heidelberg (1997)
Gupta, R.: Programming models and methods for spatiotemporal actions and reasoning in cyber-physical systems. In: NSF Workshop on CPS (2006)
Heitmeyer, C., Lynch, N.: The generalized railroad crossing: a case study in formal verification of real-time systems. In: IEEE Real-Time Systems Symposium, pp. 120–131. IEEE Computer Society Press, Los Alamitos (1994)
Laneve, C., Zavattaro, G.: Foundations of web transactions. In: Sassone, V. (ed.) FoSSaCS 2005. LNCS, vol. 3441, pp. 282–298. Springer, Heidelberg (2005)
Lee, E.A.: Cyber physical systems: design challenges. In: IEEE Symposium on Object Oriented Real-Time Distributed Computing, ISORC ’08. IEEE Computer Society, Washington (2008)
Lee, J.Y., Zic, J.: On modeling real-time mobile processes. Aust. Comput. Sci. Commun. 24(1), 139–147 (2002)
Mazzara, M.: Timing issues in web services composition. In: Bravetti, M., Kloul, L., Zavattaro, G. (eds.) EPEW/WS-EM 2005. LNCS, vol. 3670, pp. 287–302. Springer, Heidelberg (2005)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts i and ii. Inf. Comput. 100(1), 1–77 (1992)
Olate, C.: Universal temporal concurrent constraint programming. Ph.D thesis, LIX, Ecole Polytechnique (2009)
Posse, E., Dingel, J.: Theory and implementation of a real-time extension to the \(\pi \)-calculus. In: Hatcliff, J., Zucca, E. (eds.) FMOODS/FORTE 2010, Part II. LNCS, vol. 6117, pp. 125–139. Springer, Heidelberg (2010)
Saeedloei, N.: Modeling and verification of real-time and cyber-physical systems. Ph.D. thesis, University of Texas at Dallas, Richardson, Texas (2011)
Saeedloei, N., Gupta, G.: A logic-based modeling and verification of CPS. SIGBED Rev. 8, 31–34 (2011). http://doi.acm.org/10.1145/2000367.2000374
Yi, W.: CCS + time = an interleaving model for real time systems. In: Albert, J.L., Monien, B., Artalejo, M.R. (eds.) ICALP 1991. LNCS, vol. 510, pp. 217–228. Springer, Heidelberg (1991)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Saeedloei, N., Gupta, G. (2014). Timed \(\pi \)-Calculus. In: Abadi, M., Lluch Lafuente, A. (eds) Trustworthy Global Computing. TGC 2013. Lecture Notes in Computer Science(), vol 8358. Springer, Cham. https://doi.org/10.1007/978-3-319-05119-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-05119-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-05118-5
Online ISBN: 978-3-319-05119-2
eBook Packages: Computer ScienceComputer Science (R0)