论CTL和CTL+的混合扩展
计算机科学中的逻辑
2015-05-13 v1
摘要
本文研究了分支时间逻辑CTL和CTL+通过变量进行混合扩展的表达能力、相对简洁性和可满足性复杂性。先前的复杂性结果表明，只有带一个变量的片段具有初等复杂性。研究表明，H1CTL+和H1CTL（分别是CTL+和CTL带一个变量的混合扩展）在表达上等价，但H1CTL+比H1CTL指数级更简洁。另一方面，HCTL+（CTL带任意多个变量的混合扩展）不能捕捉CTL*，因为它甚至无法表达简单的CTL*性质EGFp。H1CTL+的可满足性问题是三重指数时间完全的，对于该逻辑的相当弱的片段和相当强的扩展，这一结论仍然成立。
引用
@article{arxiv.0906.2541,
title = {On the Hybrid Extension of CTL and CTL+},
author = {Ahmet Kara and Martin Lange and Thomas Schwentick and Volker Weber},
journal= {arXiv preprint arXiv:0906.2541},
year = {2015}
}