用于消息传递系统的含逆与重复算子的命题动态逻辑
计算机科学中的逻辑
2015-07-01 v2
摘要
消息序列图 (MSCs) 和通信有限状态机 (CFMs) 上的命题动态逻辑 (PDL) 的模型检测问题是指：给定信道界限 、PDL 公式 和 CFM ，判断由 接受的每个存在 -有界 MSC 是否满足 。最近的研究表明该问题是 PSPACE-完全的。在本文中，我们考虑 MSCs 上的 CRPDL，即配备了逆 (converse) 和重复 (repeat) 算子的 PDL。前者允许使用单个路径表达式在 MSC 中来回遍历，而后者允许表达路径表达式可无限次重复。为解决该逻辑的模型检测问题，我们定义了消息序列图自动机 (MSCAs)，这是一种在 MSCs 上运行的多路交替奇偶自动机。通过利用一种称为连接状态 (concatenation states) 的新概念，我们能够对每个 CRPDL 公式 归纳地构造出一个 MSCA，使其精确接受 的模型集合。结果表明，CRPDL 和 CFMs 的模型检测问题仍然属于 PSPACE。
引用
@article{arxiv.1306.3059,
title = {Propositional Dynamic Logic with Converse and Repeat for Message-Passing Systems},
author = {Roy Mennicke},
journal= {arXiv preprint arXiv:1306.3059},
year = {2015}
}