文章基本信息

标题：Counting CTL
本地全文：下载
作者：François Laroussinie ; Antoine Meyer ; Eudes Petonnet 等
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2013
卷号：9
期号：1
页码：1
DOI：10.2168/LMCS-9(1:3)2013
出版社：Technical University of Braunschweig
摘要：This paper presents a range of quantitative extensions for the temporal logic CTL. We enhance temporal modalities with the ability to constrain the number of states satisfying certain sub-formulas along paths. By selecting the combinations of Boolean and arithmetic operations allowed in constraints, one obtains several distinct logics generalizing CTL. We provide a thorough analysis of their expressiveness and succinctness, and of the complexity of their model-checking and satisfiability problems (ranging from P-complete to undecidable). Finally, we present two alternative logics with similar features and provide a comparative study of the properties of both variants.
其他关键词：branching time, counting, constraints, satisfiability, complexity.