Rule Formats for Nominal Process Calculi

TL;DR

This paper introduces rule formats for nominal residual transition systems (NRTSs) to ensure they correctly specify nominal transition systems (NTSs), applying these to the pi-calculus and exploring alternative residual specifications.

Contribution

It develops rule formats for NRTSs that guarantee they define valid NTSs and introduces translations between different residual systems, advancing the formal semantics of nominal process calculi.

Findings

Provided rule formats ensuring NRTS correctness

Applied rule formats to early and late pi-calculus

Explored and translated between residual systems with different abstraction residuals

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.