The model checking fingerprints of CTL operators
TIME '15 Proceedings of the 2015 22nd International Symposium on Temporal Representation and Reasoning (TIME)(2018)
摘要
The aim of this study is to understand the inherent expressive power of CTL operators. We investigate the complexity of model checking for all CTL fragments with one CTL operator and arbitrary Boolean operators. This gives us a fingerprint of each CTL operator. The comparison between the fingerprints yields a hierarchy of the operators that mirrors their strength with respect to model checking.
更多查看译文
关键词
Model checking,temporal logics,complexity
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要