移动信道统一理论
Unifying Theories of Mobile Channels
摘要：
在本文中，我们提出了指称语义的通道移动性的统一编程理论（UTP）的语义框架。该模型的基础是响应式进程的UTP理论（准确地说，是通信顺序进程（CSP）的UTP语义），它被稍微扩展以允许通道的移动性：一个进程被授权参与的动作集，最初是静态的或恒定的（在进程的定义过程中设置），现在是动态的或可变的：它可以在进程的执行过程中改变。因此，通过经由其他信道传送信道，然后允许接收过程用接收的信道扩展其字母表，来移动信道。新的健康条件是为了确保适当使用移动信道。
英文摘要：
In this paper we present the denotational semantics for channel mobility in the Unifying Theories of Programming (UTP) semantics framework. The basis for the model is the UTP theory of reactive processes (precisely, the UTP semantics for Communicating Sequential Processes (CSP)), which is slightly extended to allow the mobility of channels: the set of actions in which a process is authorised to participate, originally static or constant (set during the process's definition), is now made dynamic or variable: it can change during the process's execution. A channel is thus moved around by communicating it via other channels and then allowing the receiving process to extend its alphabet with the received channel. New healthiness conditions are stated to ensure an appropriate use of mobile channels.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
