分支时间时序逻辑的自动机理论刻画
计算机科学中的逻辑
2024-04-30 v2
摘要
特征定理在模型论中作为重要工具，可用于评估和比较用于形式方法中规范与验证的时序语言的表达能力。虽然在线性时间情况下，时序逻辑、谓词逻辑、代数模型和自动机之间已建立了完整的联系，但分支时间情况仍然相当零散。在这项工作中，我们通过识别两种被证明等价于这些逻辑的犹豫树自动机变体，为在任意分支树上解释的一些重要分支时间时序逻辑（即CTL*和ECTL*）提供了自动机理论刻画。这些刻画也适用于单子路径逻辑和单子链逻辑的双模拟不变片段，同样在树上解释。这些结果拓宽了分支时间情况的刻画图景，并解决了一个四十年的开放问题。
引用
@article{arxiv.2404.17421,
title = {Automata-Theoretic Characterisations of Branching-Time Temporal Logics},
author = {Massimo Benerecetti and Laura Bozzelli and Fabio Mogavero and Adriano Peron},
journal= {arXiv preprint arXiv:2404.17421},
year = {2024}
}