模型检测中状态关于迹的不完备性
计算机科学中的逻辑
2007-05-23 v2
摘要
Cousot 和 Cousot 引入并研究了一种通用的过去/未来时间规范语言，称为 mu*-calculus，其具有自然的时间对称基于迹的语义。mu*-calculus 的标准基于状态的语义是其基于迹的语义的一种抽象解释，结果表明即使对于有限系统，它也是不完备的（即迹不完备）。因此，mu*-calculus 的标准基于状态的模型检测相对于基于迹的模型检测是不完备的。本文表明，对状态集域的任何细化或抽象都会导出相应的语义，而对于 mu*-calculus 的任何命题片段，该语义仍然是迹不完备的。这源于若干结果，针对 mu*-calculus 的每个不完备的逻辑/时间连接词各一个，这些结果刻画了模型（即迁移系统）的结构，使得其对应的 mu*-calculus 基于状态的语义是迹完备的。
关键词
引用
@article{arxiv.cs/0404048,
title = {Incompleteness of States w.r.t. Traces in Model Checking},
author = {Roberto Giacobazzi and Francesco Ranzato},
journal= {arXiv preprint arXiv:cs/0404048},
year = {2007}
}