一句话:提出混合π演算 HpC,以对经典π演算的最小保守扩展统一刻画移动通信、普适性与连续物理动力学。
物联网中的网络化信息物理系统将计算基础设施置于混合、移动设备构成的动态互联网络中,其关键特征是离散通信与连续物理动力学紧密耦合,因而需要形式化手段保证正确性与可靠性。为此,作者在 Milner 经典π演算的基础上提出混合π演算 HpC,作为保守且最小的扩展:它同时刻画移动性、普适性与混合性,使网络拓扑和通信实体能够在持续演化的物理世界中变化,并允许将既有理论结果(如互模拟)提升到该扩展语境。论文以移动设备间一个真实的切换(handover)协议为例展示 HpC 的建模能力。
Networked cybernetic and physical systems of the Internet of Things (IoT) immerse civilian and industrial infrastructures into an interconnected and dynamic web of hybrid and mobile devices. The key feature of such systems is the hybrid and tight coupling of mobile and pervasive discrete communications in a continuously evolving environment (discrete computations with predominant continuous dynamics). In the aim of ensuring the correctness and reliability of such heterogeneous infrastructures, we introduce the hybrid π -calculus ( H p C ), to formally capture both mobility, pervasiveness and hybridisation in infrastructures where the network topology and its communicating entities evolve continuously in the physical world. The π -calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The H p C we propose is a conservative extension of the classical π -calculus, i.e., the extension is “minimal”, and yet describes mobility, time and physics of systems, while allowing to lift all theoretical results (e.g. bisimulation) to the context of that extension. We showcase the H p C by considering a realistic handover protocol among mobile devices.
@article{paperbot3153,
title = {HpC: A Calculus for Hybrid and Mobile Systems},
author = {Xiong Xu and Jean-Pierre Talpin and Shuling Wang and Hao Wu and Bohua Zhan and Xinxin Liu and Naijun Zhan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA1},
year = {2025},
doi = {10.1145/3720478}
}