模型检测中与轨迹相关的状态的不完整性
摘要：任何状态集合域的细化或抽象都会导致相关的语义仍然是对mu*-calculus的任何命题片段而言都是跟踪不完整的。这是由一系列结果导出的，其中每个mu*-calculus的不完整逻辑/时间连词都描述了模型的结构，即对应于mu*-calculus的状态集合语义是跟踪完整的状态转换系统。
作者：Roberto Giacobazzi and Francesco Ranzato
论文ID：cs/0404048
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2007-05-23