一次性判定所有行为等价：一种用于线性时间—分支时间谱分析的博弈
计算机科学与博弈论
2023-06-22 v6 形式语言与自动机理论
计算机科学中的逻辑
摘要
我们引入双模拟博弈的一种推广，该博弈可在 van Glabbeek 的线性时间—分支时间谱中，从两个有限状态进程之间每种有限、子公式封闭的语言找出区分性的 Hennessy-Milner 逻辑公式。我们识别衡量表达能力的相应维度，以产生属于最粗区分性行为预序与等价的公式；所比较的进程在该谱中每种更粗的行为等价下均等价。我们证明所导出的算法能确定一对进程在（不）等价中的最佳契合。
引用
@article{arxiv.2109.15295,
title = {Deciding All Behavioral Equivalences at Once: A Game for Linear-Time--Branching-Time Spectroscopy},
author = {Benjamin Bisping and David N. Jansen and Uwe Nestmann},
journal= {arXiv preprint arXiv:2109.15295},
year = {2023}
}