Abstract
We present a real-time extension to the π-calculus and use it to study a notion of time-bounded equivalence. We introduce the notion of timed compositionality and the associated timed congruence which are useful to reason about the timed behaviour of processes under hard constraints. In addition to this meta-theory we develop an abstract machine for our calculus based on event-scheduling and establish its soundness w.r.t. the given operational semantics. We have built an implementation for a realistic language called kiltera based on this machine.
This work has been funded by the Natural Sciences and Engineering Research Council of Canada (NSERC) and IBM Canada.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Berger, M.: Basic Theory of Reduction Congruence for Two Timed Asynchronous π-Calculi. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 115–130. Springer, Heidelberg (2004)
Chen, J.: A proof system for weak congruence in timed π-calculus. Tech. Report 2004-13, LIFO, Université d’Orléans (2004)
Ciobanu, G.: Behaviour Equivalences in Timed Distributed π-calculus. In: Wirsing, M., Banâtre, J.-P., Hölzl, M., Rauschmayer, A. (eds.) Soft-Ware Intensive Systems. LNCS, vol. 5380, pp. 190–208. Springer, Heidelberg (2008)
Ciobanu, G., Juravle, C.: MCTools: A Software Platform for Mobility and Timed Interaction. Tech. Report FML-09-01, Formal Methods Laboratory – Romanian Academy – Iasi Branch (February 2009)
Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 133–147. Springer, Heidelberg (1991)
Kuwabara, H., Yuen, S., Agusa, K.: Congruence Properties for a Timed Extension of the π-Calculus. In: Proc. of DSN 2005 Workshop: Dependable Software, Tools and Methods, pp. 207–214 (2005)
Lee, J.Y., Zic, J.: On modeling real-time mobile processes. In: Proc. of ACSC 2002, January 2002, pp. 139–147 (2002)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts I and II. Reports ECS-LFCS-89-85 and ECS-LFCS-89-86 86, Computer Science Dept., University of Edinburgh (March 1989)
Posse, E.: Modelling and Simulation of dynamic structure, discrete-event systems. Ph.d. thesis, School of Computer Science. McGill University (August 2008)
Posse, E.: A real-time extension to the π-calculus. Tech. Report 2009-557, School of Computing – Queen’s University (2009), http://www.cs.queensu.ca
Prisacariu, C., Ciobanu, G.: Timed Distributed π-Calculus. Tech. Report FML-05-01, Institute of Computer Science, Romanian Academy (2005)
Sangiorgi, D.: A theory of bisimulation for the π-calculus. Tech. Report ECS-LFCS-93-270, University of Edinburgh (1993)
Schneider, S.: An operational semantics for Timed CSP. Information and Computation (1995)
Turner, D.N.: The polymorphic Pi-calculus: Theory and Implementation. Ph.d. thesis, Univ. of Edinburgh (1996)
Zeigler, B.P., Praehofer, H., Kim, T.G.: Theory of modeling and simulation, 2nd edn. Academic Press, London (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Posse, E., Dingel, J. (2010). Theory and Implementation of a Real-Time Extension to the π-Calculus. In: Hatcliff, J., Zucca, E. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2010 2010. Lecture Notes in Computer Science, vol 6117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13464-7_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-13464-7_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13463-0
Online ISBN: 978-3-642-13464-7
eBook Packages: Computer ScienceComputer Science (R0)