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 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 Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.

Rule Formats for Nominal Process Calculi

Luca Aceto
;
2019

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 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 Cimini et al. and from earlier works in nominal sets and nominal logic by Gabbay, Pitts and their collaborators.
nominal sets, nominal structural operational semantics, process algebra, nominal transition systems, scope opening, rule formats
File in questo prodotto:
File Dimensione Formato  
2019_LogMethodsComputSci_15_Aceto.pdf

accesso aperto

Tipologia: Versione Editoriale (PDF)
Licenza: Creative commons
Dimensione 616.47 kB
Formato Adobe PDF
616.47 kB Adobe PDF Visualizza/Apri

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.12571/14322
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact