×

A network-conscious \(\pi\)-calculus and its coalgebraic semantics. (English) Zbl 1342.68234

Summary: Traditional process calculi usually abstract away from network details, modeling only communication over shared channels. They, however, seem inadequate to describe new network architectures, such as Software Defined Networks, where programs are allowed to manipulate the infrastructure. In this paper we present the Network Conscious \(\pi\)-calculus (NCPi), a proper extension of the \(\pi\)-calculus with an explicit notion of network: network links and nodes are represented as names, in full analogy with ordinary \(\pi\)-calculus names, and observations are routing paths through which data is transported. However, restricted links do not appear in the observations, which thus can possibly be as abstract as in the \(\pi\)-calculus. Then we construct a presheaf-based coalgebraic semantics for NCPi along the lines of Turi-Plotkin’s approach, by indexing processes with the network resources they use: we give a model for observational equivalence in this context, and we prove that it admits an equivalent nominal automaton (HD-automaton), suitable for verification. Finally, we give a concurrent semantics for NCPi where observations are multisets of routing paths. We show that bisimilarity for this semantics is a congruence, and this property holds also for the concurrent version of the \(\pi\)-calculus.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q55 Semantics in the theory of computing

Software:

KLAIM
Full Text: DOI

References:

[1] Campbell, A. T.; Katzela, I., Open signaling for atm, internet and mobile networks (opensig’98), SIGCOMM Comput. Commun. Rev., 29, 97-108 (1999)
[2] Tennenhouse, D. L.; Wetherall, D. J., Towards an active network architecture, Comput. Commun. Rev., 26, 5-18 (1996)
[3] McKeown, N.; Anderson, T.; Balakrishnan, H.; Parulkar, G. M.; Peterson, L. L.; Rexford, J.; Shenker, S.; Turner, J. S., Openflow: enabling innovation in campus networks, Comput. Commun. Rev., 38, 2, 69-74 (2008)
[4] Openflow foundation website
[5] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, i/ii, Inform. and Comput., 100, 1, 1-77 (1992) · Zbl 0752.68037
[6] Milner, R., A Calculus of Communicating Systems, Lecture Notes in Computer Science, vol. 92 (1980), Springer · Zbl 0452.68027
[7] Francalanza, A.; Hennessy, M., A theory of system behaviour in the presence of node and link failure, Inform. and Comput., 206, 6, 711-759 (2008) · Zbl 1152.68037
[8] De Nicola, R.; Gorla, D.; Pugliese, R., Basic observables for a calculus for global computing, Inform. and Comput., 205, 10, 1491-1525 (2007) · Zbl 1119.68124
[9] Corradini, A.; Montanari, U.; Rossi, F., An abstract machine for concurrent modular systems: Charm, Theoret. Comput. Sci., 122 (1&2), 165-200 (1994) · Zbl 0801.68055
[10] Fiore, M. P.; Turi, D., Semantics of name and value passing, (LICS (2001), IEEE Computer Society), 93-104
[11] Rutten, J. J.M. M., Universal coalgebra: a theory of systems, Theoret. Comput. Sci., 249, 1, 3-80 (2000) · Zbl 0951.68038
[12] Ciancia, V.; Kurz, A.; Montanari, U., Families of symmetries as efficient models of resource binding, Electron. Notes Theor. Comput. Sci., 264, 2, 63-81 (2010) · Zbl 1247.68172
[13] Montanari, U.; Pistore, M., Structured coalgebras and minimal hd-automata for the pi-calculus, Theoret. Comput. Sci., 340, 3, 539-576 (2005) · Zbl 1077.68065
[14] Ferrari, G. L.; Montanari, U.; Tuosto, E., Coalgebraic minimization of hd-automata for the pi-calculus using polymorphic types, Theoret. Comput. Sci., 331, 2-3, 325-365 (2005) · Zbl 1070.68102
[15] Lanese, I., Synchronization strategies for global computing models (2006), Computer Science Department, University of Pisa: Computer Science Department, University of Pisa Pisa, Italy, Ph.D. thesis
[16] Lanese, I., Concurrent and located synchronizations in i-calculus, (van Leeuwen, J.; Italiano, G. F.; van der Hoek, W.; Meinel, C.; Sack, H.; Plasil, F., SOFSEM (1). SOFSEM (1), Lecture Notes in Computer Science, vol. 4362 (2007), Springer), 388-399 · Zbl 1132.68044
[17] Montanari, U.; Sammartino, M., Network conscious \(π\)-calculus: A concurrent semantics, Electron. Notes Theor. Comput. Sci., 286, 291-306 (2012) · Zbl 1342.68235
[18] Sammartino, M., A network-aware process calculus for global computing and its categorical framework (2013), University of Pisa, Ph.D. thesis
[19] Lane, S. M., Categories for the Working Mathematician (1998), Springer-Verlag: Springer-Verlag New York · Zbl 0906.18001
[20] Adámek, J., Introduction to coalgebra, Theory Appl. Categ., 14, 8, 157-199 (2005) · Zbl 1080.18005
[21] Staton, S., Relating coalgebraic notions of bisimulation, Log. Methods Comput. Sci., 7, 1, 1-21 (2011) · Zbl 1247.68192
[22] Adámek, J.; Rosický, J., Locally Presentable and Accessible Categories (1994), Cambridge University Press · Zbl 0795.18007
[23] Worrell, J., Terminal sequences for accessible endofunctors, Electron. Notes Theor. Comput. Sci., 19, 24-38 (1999) · Zbl 0918.68024
[24] Staton, S., Name-passing process calculi: operational models and structural operational semantics (2007), University of Cambridge, Tech. Rep. 688
[25] Bonchi, F.; Montanari, U., Reactive systems, (semi-)saturated semantics and coalgebras on presheaves, Theoret. Comput. Sci., 410, 41, 4044-4066 (2009) · Zbl 1186.68315
[26] Bonchi, F.; Buscemi, M. G.; Ciancia, V.; Gadducci, F., A presheaf environment for the explicit fusion calculus, J. Automat. Reason., 49, 2, 161-183 (2012) · Zbl 1290.68089
[27] Gadducci, F.; Miculan, M.; Montanari, U., About permutation algebras, (pre)sheaves and named sets, High.-Order Symb. Comput., 19, 2-3, 283-304 (2006) · Zbl 1105.68083
[28] Johnstone, P., Sketches of an Elephant: A Topos Theory Compendium, Oxford Logic Guides (2002), Clarendon Press · Zbl 1071.18001
[29] Bonchi, F.; König, B.; Montanari, U., Saturated semantics for reactive systems, (LICS (2006)), 69-80
[30] Rekhter, Y., A border gateway protocol 4 (bgp-4) (March 1995)
[31] Hennessy, M.; Riely, J., Resource access control in systems of mobile agents, Inform. and Comput., 173, 1, 82-120 (2002) · Zbl 1009.68081
[32] De Nicola, R.; Ferrari, G. L.; Pugliese, R., Klaim: A kernel language for agents interaction and mobility, IEEE Trans. Software Eng., 24, 5, 315-330 (1998)
[33] De Nicola, R.; Gorla, D.; Pugliese, R., On the expressive power of klaim-based calculi, Theoret. Comput. Sci., 356, 3, 387-421 (2006) · Zbl 1092.68070
[34] Hennessy, M., A calculus for costed computations, Log. Methods Comput. Sci., 7, 1, 1-35 (2011) · Zbl 1213.68403
[35] Hennessy, M.; Gaur, M., Counting the cost in the picalculus (extended abstract), Electron. Notes Theor. Comput. Sci., 229, 3, 117-129 (2009) · Zbl 1291.68288
[36] De Vries, E.; Francalanza, A.; Hennessy, M., Reasoning about explicit resource management (extended abstract), (PLACES, ETAPS (2011)), 15-21
[37] Ghani, N.; Yemane, K.; Victor, B., Relationally staged computations in calculi of mobile processes, Electron. Notes Theor. Comput. Sci., 106, 105-120 (2004) · Zbl 1271.68183
[38] Miculan, M., A categorical model of the fusion calculus, Electron. Notes Theor. Comput. Sci., 218, 275-293 (2008) · Zbl 1286.68355
[39] Montanari, U.; Pistore, M., Concurrent semantics for the pi-calculus, Electron. Notes Theor. Comput. Sci., 1, 411-429 (1995)
[40] MacLane, S.; Moerdijk, I., Sheaves in Geometry and Logic: A First Introduction to Topos Theory, Universitext (1992), Springer · Zbl 0822.18001
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.