Counting CTL

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 of the complexity of their model-checking problem (ranging from P-complete to undecidable).

• Type: Conference
• Year: 2010
• Where: FOSSACS
• Authors: François Laroussinie, Antoine Meyer, Eudes Petonnet
• Keywords: Applied Computing, FOSSACS 2010, Logics Generalizing Ctl, Temporal Logic Ctl, Temporal Modalities