1. Andova, S., Hermanns, H., Katoen, J.-P.: Discrete-time rewards model-checked. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 88–104. Springer, Heidelberg (2004)

   Chapter  Google Scholar 

2. Baier, C., Daum, M., Dubslaff, C., Klein, J., Klüppelholz, S.: Energy-utility quantiles. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 285–299. Springer, Heidelberg (2014)

   Chapter  Google Scholar 

3. Baier, C., Klein, J., Klüppelholz, S., Wunderlich, S.: Weight monitoring with linear temporal logic: complexity and decidability. In: 23rd Conference on Computer Science Logic and the 29th Symposium on Logic In Computer Science (CSL-LICS), pp. 11:1–11:10. ACM (2014)

   Google Scholar 

4. Bauer, S.S., Juhl, L., Larsen, K.G., Srba, J., Legay, A.: A logic for accumulated-weight reasoning on multiweighted modal automata. In: 6th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 77–84. IEEE Computer Society (2012)

   Google Scholar 

5. Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. In: 26th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 43–52. IEEE Computer Society (2011)

   Google Scholar 

6. Brázdil, T., Brozek, V., Chatterjee, K., Forejt, V., Kucera, A.: Multiple mean-payoff objectives in Markov decision processes. Logical Methods in Computer Science10(1) (2014)

   Google Scholar 

7. Bruyère, V., Filiot, E., Randour, M., Raskin, J.-F.: Meet your expectations with guarantees: Beyond worst-case synthesis in quantitative games. In: 31st International Symposium on Theoretical Aspects of Computer Science (STACS), Leibniz International Proceedings in Informatics (LIPIcs), vol. 25, pp. 199–213. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2014)

   Google Scholar 

8. Chakraborty, S., Katoen, J.-P.: Parametric LTL on markov chains. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 207–221. Springer, Heidelberg (2014)

   Google Scholar 

9. Chatterjee, K., Doyen, L.: Energy and mean-payoff parity markov decision processes. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011. LNCS, vol. 6907, pp. 206–218. Springer, Heidelberg (2011)

   Chapter  Google Scholar 

10. Chatterjee, K., Doyen, L.: Energy parity games. Theoretical Computer Science458, 49–60 (2012)

    Article MathSciNet MATH  Google Scholar 

11. Chatterjee, K., Doyen, L., Randour, M., Raskin, J.-F.: Looking at mean-payoff and total-payoff through windows. Information and Computation242, 25–52 (2015)

    Article MathSciNet MATH  Google Scholar 

12. Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. Journal of the ACM62(1), 9:1–9:34 (2015)

    Article MathSciNet MATH  Google Scholar 

13. Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM42(4), 857–907 (1995)

    Article MathSciNet MATH  Google Scholar 

14. de Alfaro, L.: Formal Verification of Probabilistic Systems. Ph.D. thesis, Stanford University, Department of Computer Science (1997)

    Google Scholar 

15. Dräger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 531–546. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

16. Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Logical Methods in Computer Science4(4) (2008)

    Google Scholar 

17. Grötschel, M., Lovász, L., Schrijver, A.: Geometric Algorithms and Combinatorial Optimization. Springer (1993)

    Google Scholar 

18. Haase, C., Kiefer, S.: The odds of staying on budget. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 234–246. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

19. Juhl, L., Guldstrand Larsen, K., Raskin, J.-F.: Optimal bounds for multiweighted and parametrised energy games. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 244–255. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

20. Krähmann, D., Schubert, J., Baier, C., Dubslaff, C.: Ratio and weight quantiles. In: Italiano, G.F., Pighizzini, G., Sannella, D.T. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 344–356. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

21. Laroussinie, F., Sproston, J.: Model checking durational probabilistic systems. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, pp. 140–154. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

22. Randour, M., Raskin, J.-F., Sankur, O.: Percentile queries in multi-dimensional markov decision processes. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 123–139. Springer, Heidelberg (2015)

    Chapter  Google Scholar 

23. Tomita, T., Hiura, S., Hagihara, S., Yonezaki, N.: A temporal logic with mean-payoff constraints. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 249–265. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

24. Ummels, M., Baier, C.: Computing quantiles in markov reward models. In: Pfenning, F. (ed.) FOSSACS 2013 (ETAPS 2013). LNCS, vol. 7794, pp. 353–368. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

25. Velner, Y., Chatterjee, K., Doyen, L., Henzinger, T.A., Rabinovich, A.M., Raskin, J.-F.: The complexity of multi-mean-payoff and multi-energy games. Information and Computation241, 177–196 (2015)

    Article MathSciNet MATH  Google Scholar 

26. von Essen, C., Jobstmann, B.: Synthesizing efficient controllers. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 428–444. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

Download references