Document Open Access Logo

Rule Formats for Nominal Process Calculi

Authors Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, Yolanda Ortega-Mallén

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2017.10.pdf
  • Filesize: 0.53 MB
  • 16 pages

Document Identifiers

Author Details

Luca Aceto
Ignacio Fábregas
Álvaro García-Pérez
Anna Ingólfsdóttir
Yolanda Ortega-Mallén

Cite AsGet BibTex

Luca Aceto, Ignacio Fábregas, Álvaro García-Pérez, Anna Ingólfsdóttir, and Yolanda Ortega-Mallén. Rule Formats for Nominal Process Calculi. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 10:1-10:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CONCUR.2017.10

Abstract

The nominal transition systems (NTSs) of Parrow et al. 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 specification of the early pi-calculus. Our study stems from the recent Nominal SOS of Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.
Keywords
  • nominal sets
  • nominal structural operational semantics
  • process algebra
  • nominal transition systems
  • scope opening
  • rule formats

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. L. Aceto, M. Cimini, M. J. Gabbay, A. Ingólfsdóttir, M. R. Mousavi, and M. A. Reniers. Nominal structural operational semantics. In preparation. Google Scholar
  2. L. Aceto, W. Fokkink, and C. Verhoef. Structural operational semantics. In Handbook of Process Algebra, chapter 3, pages 197-292. Elsevier, 2001. Google Scholar
  3. L. Aceto, I. Fábregas, Á. García-Pérez, and A. Ingólfsdóttir. A unified rule format for bounded nondeterminism in SOS with terms as labels. Journal of Logical and Algebraic Methods in Programming, 2017. URL: http://dx.doi.org/10.1016/j.jlamp.2017.03.002.
  4. J. Bengtson and J. Parrow. Formalising the pi-calculus using nominal logic. Logical Methods in Computer Science, 5(2), 2009. URL: http://dx.doi.org/10.2168/LMCS-5(2:16)2009.
  5. 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. URL: http://dx.doi.org/10.1109/LICS.1998.705652.
  6. S. Burris and H. P. Sankappanavar. A Course in Universal Algebra: The Millennium Edition. Springer Verlag, 2000. Google Scholar
  7. M. Cimini, M. R. Mousavi, M. A. Reniers, and M. J. Gabbay. Nominal SOS. Electronic Notes in Theoretical Computer Science, 286:103-116, 2012. URL: http://dx.doi.org/10.1016/j.entcs.2012.08.008.
  8. R. Clouston and A. Pitts. Nominal equational logic. Electronic Notes in Theoretical Computer Science, 172:223-257, 2007. URL: http://dx.doi.org/10.1016/j.entcs.2007.02.009.
  9. M. Fernández and M. J. Gabbay. Nominal rewriting. Information and Computation, 205(6):917-965, 2007. URL: http://dx.doi.org/10.1016/j.ic.2006.12.002.
  10. M. P. Fiore and S. Staton. A congruence rule format for name-passing process calculi. Information and Computation, 207(2):209-236, 2009. URL: http://dx.doi.org/10.1016/j.ic.2007.12.005.
  11. 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. URL: http://dx.doi.org/10.1109/LICS.2001.932486.
  12. 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. URL: http://dx.doi.org/10.1016/j.tcs.2005.11.035.
  13. W. Fokkink and C. Verhoef. A conservative look at operational semantics with variable binding. Information and Computation, 146(1):24-54, 1998. URL: http://dx.doi.org/10.1006/inco.1998.2729.
  14. W. Fokkink and T. D. Vu. Structural operational semantics and bounded nondeterminism. Acta Informatica, 39(6-7):501-516, 2003. URL: http://dx.doi.org/10.1007/s00236-003-0111-1.
  15. 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. URL: http://dx.doi.org/10.1093/logcom/exp033.
  16. M. J. Gabbay and A. Mathijssen. A nominal axiomatization of the lambda calculus. Journal of Logic and Computation, 20(2):501-531, 2010. URL: http://dx.doi.org/10.1093/logcom/exp049.
  17. 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. URL: http://dx.doi.org/10.1007/s001650200016.
  18. 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. URL: http://dx.doi.org/10.1145/321992.321997.
  19. C. A. Middelburg. Variable binding operators in transition system specifications. Journal of Logic and Algebraic Programming, 47(1):15-45, 2001. URL: http://dx.doi.org/10.1016/S1567-8326(00)00003-5.
  20. C. A. Middelburg. An alternative formulation of operational conservativity with binding terms. Journal of Logic and Algebraic Programming (JLAP), 55(1-2):1-19, 2003. URL: http://dx.doi.org/10.1016/S1567-8326(02)00039-5.
  21. R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes (Parts I and II). Information and Computation, 100(1):1-77, 1992. URL: http://dx.doi.org/10.1016/0890-5401(92)90008-4.
  22. 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. URL: http://dx.doi.org/10.1016/j.tcs.2006.12.019.
  23. J. Parrow, J. Borgström, L.-H. Eriksson, R. Gutkovas, and T. Weber. Modal logics for nominal transition systems. In 26th International Conference on Concurrency Theory, volume 42 of LIPIcs, pages 198-211. Schloss Dagstuhl, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CONCUR.2015.198.
  24. J. Parrow, T. Weber, J. Borgström, 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. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-319-60225-7_13.
  25. A. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, 2013. Google Scholar
  26. A. Pitts. Nominal techniques. ACM SIGLOG News, 3(1):57-72, 2016. URL: http://dx.doi.org/10.1145/2893582.2893594.
  27. G. D. Plotkin. A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60-61:17-139, 2004. Google Scholar
  28. D. Sangiorgi. pi-Calculus, internal mobility, and agent-passing calculi. Theoretical Computer Science, 167(1&2):235-274, 1996. URL: http://dx.doi.org/10.1016/0304-3975(96)00075-8.
  29. D. Sangiorgi and D. Walker. The π-calculus - A Theory of Mobile Processes. Cambridge University Press, 2001. Google Scholar
  30. C. Urban, A. Pitts, and M. J. Gabbay. Nominal unification. Theoretical Computer Science, 323(1-3):473-497, 2004. URL: http://dx.doi.org/10.1016/j.tcs.2004.06.016.
  31. 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. URL: http://dx.doi.org/10.1016/j.entcs.2005.09.032.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact