HpC: A Calculus for Hybrid and Mobile Systems - Full Version

作     者：Xu, Xiong Talpin, Jean-Pierre Wang, Shuling Wu, Hao Zhan, Bohua Liu, Xinxin Zhan, Naijun 

作者机构：National Key Laboratory of Space Integrated Information System Institute of Software Chinese Academy of Sciences Beijing China INRIA Centre INRIA à l’Université de Rennes France and SKLCS Institute of Software Chinese Academy of Sciences UCAS Beijing China Huawei Technologies Co. Ltd. Beijing China and SKLCS Institute of Software Chinese Academy of Sciences Beijing China School of Computer Science Peking University Beijing China 

出 版 物：《arXiv》 (arXiv)

年 卷 期：2025年

核心收录：

主　　题：Mobile telecommunication systems 

摘      要：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 c-calculus (HpC), 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 c-calculus proposed by Robin Milner et al. is a process calculus that can model mobile communications and computations in a very elegant manner. The HpC we propose is a conservative extension of the classical c-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 HpC by considering a realistic handover protocol among mobile devices. © 2025, CC BY.