论文部分内容阅读
首先,给出了基于广义可能性测度的计算树逻辑的扩展GPoCTL＊、计算树逻辑的约简GPoCTL^-以及带回报的计算树逻辑GPoRCTL的语构和语义。在经典互模拟和广义可能性测度的基础上讨论了广义可能性互模拟及其相关性质。最后证明了GPoCTL、GPoCTL＊和GPoCTL^-公式与互模拟状态之间的等价关系。