Abstract : 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).
https://hal.archives-ouvertes.fr/hal-00681263 Contributor : Antoine MeyerConnect in order to contact the contributor Submitted on : Wednesday, March 21, 2012 - 9:43:56 AM Last modification on : Saturday, January 15, 2022 - 3:59:31 AM Long-term archiving on: : Friday, June 22, 2012 - 2:21:13 AM