一句话：提出名义剩余迁移系统及其规则格式，保证其对应名义迁移系统，并应用于π演算。
名义迁移系统（NTS）由 Parrow 等人提出，用于刻画名义进程演算的操作语义，但其规格何时确实产生 NTS 尚缺通用判据。本文引入名义剩余迁移系统（NRTS）来研究 NTS，并给出 NRTS 规格的规则格式，保证所得 NRTS 同时也是 NTS；作者将该格式应用于 early 与 late π-演算的操作规格，验证其适用性。论文还探讨允许 abstraction sort 剩余项的 NTS 替代规格，并在含与不含 abstraction sort 剩余项的系统之间建立翻译，从而统一并扩展 Cimini 等人的 Nominal SOS 及 Gabbay、Pitts 等关于名义集合与名义逻辑的工作。
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.
@article{paperbot751,
title = {Rule Formats for Nominal Process Calculi},
author = {Luca Aceto and Ignacio Fábregas and Álvaro García-Pérez and Anna Ingólfsdóttir and Yolanda Ortega-Mallén},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 4},
year = {2019},
doi = {10.23638/lmcs-15(4:2)2019}
}