标记迁移系统作为石空间

展示了一种对于模态迁移系统及其细化的全抽象且通用的域模型，即标记迁移系统在有限事件集合上的二分相似商的maximal-points空间模型。在该域模型中，我们证明了该商是石空间，其紧凑、零维且ultra-metrizable的Hausdorff拓扑度量了二分相似程度，使得图像有限的标记迁移系统稠密。利用这种紧凑性，我们证明了标记迁移系统的实现集——即细化模态迁移系统的所有标记迁移系统的集合——是紧凑的，并推导出关于此类实现集的Hennessy-Milner逻辑的紧凑性定理。这些结果推广到也具有部分指定状态命题的系统，统一了现有的关于部分过程的归纳、操作和度量语义，使模态迁移系统的一致性度量更为稳健，并将标记迁移系统的紧凑集作为模态迁移系统的Scott闭集进行抽象解释。