连续时间中 Kahn 网络的非标准语义

在一篇开创性的文章中，Kahn 引入了进程网络的概念，并使用元素为（可能是无限的）值序列的 Scott 域为其给出了语义。此后，该模型成为研究分布式异步计算的标准工具。从一开始，进程网络就被绘制为特定的图，但这种语法从未被形式化。我们借此机会通过给出这些图（我们称之为网）的精确定义来澄清这一点。由此产生的范畴被证明是一个不动点范畴，即一个关于由积给出的幺半结构具有迹的笛卡尔范畴，有趣的是，该结构刻画了这个范畴：我们证明了它是包含给定态射集的自由不动点范畴，从而为进程网络模型应满足的公理体系提供了完备的基础。然后，我们使用这些工具构建了一个数据在连续时间上变化的网络模型，以阐述进程网络也应能涵盖混合系统或电路等计算模型的思想。我们通过引入基于非标准分析的第三个网络模型，将该模型与 Kahn 的语义联系起来，该模型的元素构成一个内部完全偏序，标准域的许多性质可以在其中重新表述。该模型中对超实数的使用使其能够形式化地考虑无穷小的概念，从而在离散时间和连续时间之间架起桥梁：时间是“离散”的，但两个时刻之间的持续时间是无穷小的。最后，我们通过描述一些实现分析中常见构造的网络，给出了该模型应用的一些示例。