关于CTL和CTL +的混合扩张
On the Hybrid Extension of CTL and CTL+
摘要：
本文研究了分支时间逻辑CTL和CTL+的变量混合扩张的可满足性的表达性、相对简洁性和复杂性。以前的复杂性结果表明，只有一个变量的片段具有基本复杂性。结果表明，H1CTL+和H1CTL，分别与一个变量的CTL+和CTL的混合扩展，是表示等价的，但H1CTL+是指数更简洁比H1CTL。另一方面，具有任意多个变量的CTL的混合扩展HCTL+不捕获CTL*，因为它甚至不能表达简单的CTL* 属性EGFp。H1CTL+的可满足性问题对于三重指数时间是完全的，这对于逻辑的相当弱的片段和相当强的扩展仍然成立。
英文摘要：
The paper studies the expressivity, relative succinctness and complexity of satisfiability for hybrid extensions of the branching-time logics CTL and CTL+ by variables. Previous complexity results show that only fragments with one variable do have elementary complexity. It is shown that H1CTL+ and H1CTL, the hybrid extensions with one variable of CTL+ and CTL, respectively, are expressively equivalent but H1CTL+ is exponentially more succinct than H1CTL. On the other hand, HCTL+, the hybrid extension of CTL with arbitrarily many variables does not capture CTL*, as it even cannot express the simple CTL* property EGFp. The satisfiability problem for H1CTL+ is complete for triply exponential time, this remains true for quite weak fragments and quite strong extensions of the logic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
