S. Almagor, U. Boker, and O. Kupferman, Formalizing and Reasoning about Quality, ICALP'13, pp.15-27, 2013.
DOI : 10.1007/978-3-642-39212-2_3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.294.6885

S. Almagor, U. Boker, and O. Kupferman, Discounting in LTL, TACAS'14, 2014.
DOI : 10.1007/978-3-642-54862-8_37

S. Almagor, U. Boker, and O. Kupferman, Discounting in LTL
DOI : 10.1007/978-3-642-54862-8_37

R. Alur and D. L. Dill, A theory of timed automata, Theoretical Computer Science, vol.126, issue.2, pp.183-235, 1994.
DOI : 10.1016/0304-3975(94)90010-8

R. Alur, S. L. Torre, and G. J. Pappas, Optimal paths in weighted timed automata, HSCC'01, pp.49-62, 2001.

A. Aziz, K. Sanwal, V. Singhal, and R. K. Brayton, Model-checking continuous-time Markov chains, ACM Transactions on Computational Logic, vol.1, issue.1, pp.162-170, 2000.
DOI : 10.1145/343369.343402
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.18.8774

G. Behrmann, A. Fehnker, T. Hune, K. G. Larsen, P. Pettersson et al., Minimum-Cost Reachability for Priced Timed Automata, HSCC'01, pp.147-161, 2001.
DOI : 10.7146/brics.v8i3.20457

U. Boker, K. Chatterjee, T. A. Henzinger, and O. Kupferman, Temporal specifications with accumulative values, LICS'11, pp.43-52, 2011.

B. Bollig, N. Decker, and M. Leucker, Frequency Linear-time Temporal Logic, 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering, pp.85-92, 2012.
DOI : 10.1109/TASE.2012.43
URL : https://hal.archives-ouvertes.fr/hal-00776769

P. Bouyer, P. Gardy, and N. Markey, Quantitative Verification of Weighted Kripke Structures, 2014.
DOI : 10.1007/978-3-319-11936-6_6

P. Bouyer, N. Markey, R. M. Matteplackel, T. A. Henzinger, and A. Radhakrishna, Quantitative verification of weighted kripke structures Research Report LSV-14-02 Simulation distances, Theor. Computer Science, vol.413, issue.1, pp.21-35, 2012.

K. Chatterjee, L. Doyen, and T. A. Henzinger, Quantitative languages, ACM Transactions on Computational Logic, vol.11, issue.4, 2010.
DOI : 10.1145/1805950.1805953
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.9296

L. De-alfaro, M. Faella, T. A. Henzinger, R. Majumdar, and M. Stoelinga, Model checking discounted temporal properties, Theoretical Computer Science, vol.345, issue.1, pp.139-170, 2005.
DOI : 10.1016/j.tcs.2005.07.033

L. Doyen, Games and Automata: From Boolean to Quantitative Verification. Mémoire d'habilitation, 2012.

M. Faella, A. Legay, and M. Stoelinga, Model Checking Quantitative Linear Time Logic, QAPL'08, pp.61-77, 2008.
DOI : 10.1016/j.entcs.2008.11.019

T. A. Henzinger, Quantitative Reactive Models, MODELS'12, pp.1-2, 2012.
DOI : 10.1007/978-3-642-33666-9_1

T. A. Henzinger and J. Otop, From Model Checking to Model Measuring, CONCUR'13, pp.273-287, 2013.
DOI : 10.1007/978-3-642-40184-8_20

M. L. Minsky, Computation: Finite and Infinite Machines, 1967.

M. Schützenberger, On the definition of a family of automata, Information and Control, vol.4, issue.2-3, pp.245-270, 1961.
DOI : 10.1016/S0019-9958(61)80020-X

T. Tomita, S. Hiura, S. Hagihara, and N. Yonezaki, A temporal logic with meanpayoff constraints, ICFEM'12, pp.249-265, 2012.