真并发可以很简单
计算机科学中的逻辑
2023-01-31 v3
摘要
步网互模拟是有限 Petri 网的一种协归纳行为关系，它是有限 Petri 网上标准步互模拟 \cite{NT84} 定义的平滑推广。其所导出的等价关系为因果网互模拟 \cite{G15,Gor22} 提供了一种替代性的、简单得多的刻画——因为它不借助任何因果结构；也为保结构互模拟 \cite{G15} 提供了替代性刻画——因为它不要求相关标识间的双射映射。我们证明步网互模拟可通过一种合适的模态逻辑（称为 NML，即网模态逻辑 net modal logic 的缩写）从逻辑上刻画：两个标识是步网互模拟的，当且仅当它们满足相同的 NML 公式。
引用
@article{arxiv.2211.00557,
title = {True Concurrency Can Be Easy},
author = {Roberto Gorrieri},
journal= {arXiv preprint arXiv:2211.00557},
year = {2023}
}
备注
Incorrect