Abstract
This paper introduces the π-graphs, a graphical model of mobile interactions that tries to accommodate the expressivity of the π-calculus and the intuitiveness of place-transition nets. Graph rewriting techniques are used to describe the operational semantics of π-graphs. The bijective encoding/decoding of π-graphs allows to mix transparently graphical and term-based proof techniques, which leads to a dual characterization of bisimilarity. The main originality of this characterization is the synchronous interpretation it provides: each graph/term being attached to a clock evolving at the rate of interactions with the environment. This gives new opportunities for the design of efficient verification algorithms for mobile systems.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Milner, R.: Communicating and Mobile Systems: The π-Calculus. Cambridge University Press, Cambridge (1999)
Milner, R.: Pi-nets: A graphical form of pi-calculus. In: Sannella, D. (ed.) ESOP 1994. LNCS, vol. 788, pp. 26–42. Springer, Heidelberg (1994)
Parrow, J.: Interaction diagrams. Nord. J. Comput. 2, 407–443 (1995)
Gadducci, F., Montanari, U.: Observing reductions in nominal calculi via a graphical encoding of processes. In: Middeldorp, A., van Oostrom, V., van Raamsdonk, F., de Vrijer, R. (eds.) Processes, Terms and Cycles: Steps on the Road to Infinity. LNCS, vol. 3838, pp. 106–126. Springer, Heidelberg (2005)
Laneve, C., Parrow, J., Victor, B.: Solo diagrams. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 127–144. Springer, Heidelberg (2001)
Gadducci, F.: Graph rewriting for the π-calculus. Mathematical Structures in Computer Science 17, 407–437 (2007)
Victor, B., Moller, F.: The mobility workbench - a tool for the pi-calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 428–440. Springer, Heidelberg (1994)
Pistore, M., Sangiorgi, D.: A partition refinement algorithm for the π-calculus. Inf. Comput. 164, 264–321 (2001)
Peschanski, F.: A tutorial on π-graphs: diagrams of mobile interactions. Technical report, LIP6 - UPMC Paris Universitas (2008), http://www-poleia.lip6.fr/~pesch/pigraphs
Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21, 558–565 (1978)
Löwe, M.: Algebraic approach to single-pushout graph transformation. Theor. Comput. Sci. 109, 181–224 (1993)
Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16, 973–989 (1987)
Rozenberg, G. (ed.): Handbook of graph grammars and computing by graph transformation: volume I. foundations. World Scientific Publishing Co., Inc., River Edge (1997)
Ferrari, G.L., Gnesi, S., Montanari, U., Pistore, M., Ristori, G.: Verifying mobile processes in the hal environment. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 511–515. Springer, Heidelberg (1998)
Devillers, R.R., Klaudel, H., Koutny, M.: Modelling mobility in high-level petri nets. In: ACSD, pp. 110–119. IEEE Computer Society, Los Alamitos (2007)
Montanari, U., Pistore, M.: pi-calculus, structured coalgebras, and minimal hd-automata. In: Nielsen, M., Rovan, B. (eds.) MFCS 2000. LNCS, vol. 1893, pp. 569–578. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Peschanski, F., Bialkiewicz, JA. (2009). Modelling and Verifying Mobile Systems Using π-Graphs. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds) SOFSEM 2009: Theory and Practice of Computer Science. SOFSEM 2009. Lecture Notes in Computer Science, vol 5404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-95891-8_40
Download citation
DOI: https://doi.org/10.1007/978-3-540-95891-8_40
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-95890-1
Online ISBN: 978-3-540-95891-8
eBook Packages: Computer ScienceComputer Science (R0)