Counting LTL F. Laroussinie, A. Meyer, E. Petonnet TIME 2010 This paper presents a quantitative extension for the linear-time temporal logic LTL in order to specify the number of states satisfying certain sub-formulas along paths. We give decision procedures (model checking and satisfiability) for this new temporal logic. We also study the complexity of the corresponding problems. Finally we show that the problems become undecidable when more powerful contraints are allowed in the formulas.