过去的荣耀与几何并发性

本文有助于加深对 Pratt 命名为高维自动机（HDA）的并发几何模型的一般理解。我们特别研究了此类模型的模态逻辑及其在可捕获的互模拟方面的表达能力。并发几何模型因其通用性和表达能力，以及自动并发和动作精化被自然捕获的方式而引人关注。然而，该模型的逻辑尚未得到充分研究，直到最近才引入了一种简单但足够的、基于 HDA 的模态逻辑。由于这种包含两个存在性模态（during 和 after）的模态逻辑仅捕获分裂互模拟，这在 van Glabbeek 和 Vaandrager 的谱系中处于较低位置，因此一个直接的问题是，该逻辑的何种小扩展能够捕获更细粒度的遗传历史保持互模拟（hh）。作为回应，本文的工作提供了若干见解。其一是，HDA 的几何方面使得使用一种不采用事件变量的标准模态逻辑来捕获 hh-互模拟成为可能，这与我们比较的两种逻辑（基于表达能力较弱的模型）相反。我们在此研究的逻辑使用了标准的过去模态，并扩展了先前引入的仅具有前向、动作标记模态的逻辑（称为 HDML）。此外，我们通过引入一个称为 ST-配置结构的相关模型来更好地理解上述问题，该模型扩展了 van Glabbeek 和 Plotkin 的配置结构。我们将该模型与 HDA 联系起来，并基于这一新模型重新定义和证明了先前的结果。这为过去模态和几何并发性为何能捕获遗传历史保持互模拟提供了不同的视角。还获得了其他相关的见解。