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.

翻译：Parrow等人的标称迁移系统描述了标称进程演算的操作语义。我们从新引入的标称剩余迁移系统角度对标称迁移系统进行研究。我们为标称剩余迁移系统的规格说明提供了规则格式，确保相应的标称剩余迁移系统构成一个标称迁移系统，并将这些格式应用于早期π-演算的操作规格说明。本研究源于Cimini等人近期提出的标称SOS框架，以及Gabbay、Pitts及其合作者在标称集合与标称逻辑方面的早期工作。