×

Rule formats for nominal process calculi. (English) Zbl 1442.68119

Summary: The nominal transition systems (NTSs) of J. Parrow et al. [LIPIcs – Leibniz Int. Proc. Inform. 42, 198–211 (2015; Zbl 1374.68339)] describe the operational semantics of nominal process calculi. We study NTSs in terms of the nominal residual transition systems (NRTSs) that we introduce. We provide rule formats for the specifications of NRTSs that ensure that the associated NRTS is an NTS and apply them to the operational specifications of the early and late pi-calculus. We also explore alternative specifications of the NTSs in which we allow residuals of abstraction sort, and introduce translations between the systems with and without residuals of abstraction sort. Our study stems from the Nominal SOS of M. Cimini et al. [Electron. Notes Theor. Comput. Sci. 286, 103–116 (2012; Zbl 1342.68193)] and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B70 Logic in computer science
68Q55 Semantics in the theory of computing
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Freshml
PDFBibTeX XMLCite
Full Text: arXiv

References:

[1] [ABI+12]L. Aceto, A. Birgisson, A. Ing´olfsd´ottir, M. R. Mousavi, and M. A. Reniers. Rule formats for determinism and idempotence. Science of Computer Programming, 77(7-8):889-907, 2012. · Zbl 1243.68205
[2] [ACCL91]M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. L´evy. Explicit substitutions. Journal of Functional Programming, 1(4):375-416, 1991. · Zbl 0941.68542
[3] [ACG+]L. Aceto, M. Cimini, M. J. Gabbay, A. Ing´olfsd´ottir, M. R. Mousavi, and M. A. Reniers. Nominal structural operational semantics. In preparation.
[4] [AFGI17]L. Aceto, I. F´abregas, A. Garc´ıa-P´erez, and A. Ing´olfsd´ottir. A unified rule format for bounded nondeterminism in SOS with terms as labels. Journal of Logical and Algebraic Methods in
[5] [AFGP+17] L. Aceto, I. F´abregas, A. Garc´ıa-P´erez, A. Ing´olfsd´ottir, and Y. Ortega-Mall´en. Rule formats for nominal process calculi. In 28th International Conference on Concurrency Theory, volume 85 of · Zbl 1442.68120
[6] [AFV01]L. Aceto, W. Fokkink, and C. Verhoef. Structural operational semantics. In Handbook of Process · Zbl 1062.68074
[7] [Ber98]K. L. Bernstein. A congruence theorem for structured operational semantics of higher-order languages. In 13th Annual IEEE Symposium on Logic in Computer Science, pages 153-164. IEEE Computer Society, 1998.
[8] [BP09]J. Bengtson and J. Parrow. Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science, 5(2), 2009. · Zbl 1168.68030
[9] [BS00]S. Burris and H. P. Sankappanavar. A Course in Universal Algebra: The Millennium Edition. Springer Verlag, 2000.
[10] [CMRG12]M. Cimini, M. R. Mousavi, M. A. Reniers, and M. J. Gabbay. Nominal SOS. Electronic Notes in Theoretical Computer Science, 286:103-116, 2012. · Zbl 1342.68193
[11] [CP07]R. Clouston and A. Pitts. Nominal equational logic. Electronic Notes in Theoretical Computer Science, 172:223-257, 2007. · Zbl 1277.68043
[12] [FG07]M. Fern´andez and M. J. Gabbay. Nominal rewriting. Information and Computation, 205(6):917- 965, 2007. · Zbl 1118.68075
[13] [FS09]M. P. Fiore and S. Staton. A congruence rule format for name-passing process calculi. Information and Computation, 207(2):209-236, 2009. · Zbl 1165.68050
[14] [FT01]M. P. Fiore and D. Turi. Semantics of name and value passing. In 16th Annual IEEE Symposium on Logic in Computer Science, pages 93-104. IEEE Computer Society, 2001.
[15] [FV98]W. Fokkink and C. Verhoef. A conservative look at operational semantics with variable binding. Information and Computation, 146(1):24-54, 1998. · Zbl 0916.68098
[16] [FV03]W. Fokkink and T. D. Vu. Structural operational semantics and bounded nondeterminism. Acta Informatica, 39(6-7):501-516, 2003. · Zbl 1060.68070
[17] [FvGdW06] W. Fokkink, R. J. van Glabbeek, and P. de Wind. Compositionality of Hennessy-Milner logic by structural operational semantics. Theoretical Computer Science, 354(3):421-440, 2006. · Zbl 1088.68094
[18] [GH08]M. J. Gabbay and M. Hofmann. Nominal renaming sets. In Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, volume 5330 of Lecture Notes in · Zbl 1182.03065
[19] [GM09]M. J. Gabbay and A. Mathijssen. Nominal (universal) algebra: Equational logic with names and binding. Journal of Logic and Computation, 19(6):1455-1508, 2009. · Zbl 1191.08003
[20] [GM10]M. J. Gabbay and A. Mathijssen. A nominal axiomatization of the lambda calculus. Journal of Logic and Computation, 20(2):501-531, 2010. · Zbl 1198.03023
[21] [GP02]M. J. Gabbay and A. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects of Computing, 13(3-5):341-363, 2002. · Zbl 1001.68083
[22] [GTWW77] J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebras. Journal of the ACM, 24(1):68-95, 1977. · Zbl 0359.68018
[23] [GV92]J. F. Groote and F. W. Vaandrager. Structured operational semantics and bisimulation as a congruence. Information and Computation, 100(2):202-260, 1992. · Zbl 0752.68053
[24] [Lam68]J. Lambek. A fixed point theorem for complete categories. Mathematische Zeitung, 103:151-161, 1968. · Zbl 0149.26105
[25] [Mid01]C. A. Middelburg. Variable binding operators in transition system specifications. Journal of Logic and Algebraic Programming, 47(1):15-45, 2001. · Zbl 0970.68117
[26] [Mid03]C. A. Middelburg. An alternative formulation of operational conservativity with binding terms. Journal of Logic and Algebraic Programming, 55(1-2):1-19, 2003. · Zbl 1048.68056
[27] [MPW92]R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (Parts I and II). Information and Computation, 100(1):1-77, 1992. · Zbl 0752.68037
[28] [MRG07]M. R. Mousavi, M. A. Reniers, and J. F. Groote. SOS formats and meta-theory: 20 years after. Theoretical Computer Science, 373(3):238-272, 2007. · Zbl 1111.68069
[29] [MT05]D. Miller and A. Tiu. A proof theory for generic judgments. ACM Transactions on Computational Logic, 6(4):749-783, 2005. · Zbl 1367.03059
[30] [Par18]J. Parrow. Nominal transition systems defined by name abstraction, 2018. Personal communication.
[31] [PBE+15]J. Parrow, J. Borgstr¨om, L.-H. Eriksson, R. Gutkovas, and T. Weber. Modal logics for nominal transition systems. In 26th International Conference on Concurrency Theory, volume 42 of · Zbl 1374.68339
[32] [Pit13]A. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. · Zbl 1297.68008
[33] [Pit16]A. Pitts. Nominal techniques. ACM SIGLOG News, 3(1):57-72, 2016.
[34] [Plo04]G. D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17-139, 2004. · Zbl 1082.68062
[35] [PWBE17]J. Parrow, T. Weber, J. Borgstr¨om, and L.-H. Eriksson. Weak nominal modal logic. In Formal Techniques for Distributed Objects, Components, and Systems - 37th IFIP WG 6.1 International Conference, FORTE 2017, volume 10321 of Lecture Notes in Computer Science, pages 179-193. · Zbl 1489.68167
[36] [San96]D. Sangiorgi. pi-Calculus, internal mobility, and agent-passing calculi. Theoretical Computer Science, 167(1&2):235-274, 1996. · Zbl 0874.68103
[37] [SPG03]M. R. Shinwell, A. Pitts, and M. J. Gabbay. FreshML: programming with binders made simple. SIGPLAN Notices, 38(9):263-274, 2003. · Zbl 1315.68058
[38] [SW01]D. Sangiorgi and D. Walker. The π-calculus — A Theory of Mobile Processes. Cambridge University Press, 2001. · Zbl 0981.68116
[39] [UPG04]C. Urban, A. Pitts, and M. J. Gabbay. Nominal unification. Theoretical Computer Science, 323(1-3):473-497, 2004. · Zbl 1078.68140
[40] [ZMP06]A. Ziegler, D. Miller, and C. Palamidessi. A congruence format for name-passing calculi. Electronic Notes in Theoretical Computer Science, 156(1):169-189, 2006. · Zbl 1273.68216
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.