{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:14:31Z","timestamp":1748751271143,"version":"3.41.0"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319287652"},{"type":"electronic","value":"9783319287669"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-28766-9_8","type":"book-chapter","created":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T12:09:44Z","timestamp":1451909384000},"page":"112-130","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Near-Optimal Scheduling for LTL with Future Discounting"],"prefix":"10.1007","author":[{"given":"Shota","family":"Nakagawa","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,5]]},"reference":[{"issue":"2","key":"8_CR1","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1016\/j.tcs.2005.11.018","volume":"354","author":"Y Abdedda\u00efm","year":"2006","unstructured":"Abdedda\u00efm, Y., Asarin, E., Maler, O.: Scheduling with timed automata. Theor. Comput. Sci. 354(2), 272\u2013300 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-39212-2_3","volume-title":"Automata, Languages, and Programming","author":"S Almagor","year":"2013","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. In: Fomin, F.V., Freivalds, R., Kwiatkowska, M., Peleg, D. (eds.) ICALP 2013, Part II. LNCS, vol. 7966, pp. 15\u201327. Springer, Heidelberg (2013)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/978-3-642-54862-8_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Almagor","year":"2014","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Discounting in LTL. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 424\u2013439. Springer, Heidelberg (2014)"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. Extended version of [2], preprint (private communication) (2014)","DOI":"10.1007\/978-3-642-39212-2_3"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Baier, C., Dubslaff, C., Kl\u00fcppelholz, S.: Trade-off analysis meets probabilistic model checking. In: Henzinger, T.A., Miller, D. (eds.), CSL-LICS 2014, p. 1. ACM (2014)","DOI":"10.1145\/2603088.2603089"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140\u2013156. Springer, Heidelberg (2009)"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/978-3-662-44584-6_19","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"P Bouyer","year":"2014","unstructured":"Bouyer, P., Markey, N., Matteplackel, R.M.: Averaging in LTL. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 266\u2013280. Springer, Heidelberg (2014)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-22110-1_20","volume-title":"Computer Aided Verification","author":"P \u010cern\u00fd","year":"2011","unstructured":"\u010cern\u00fd, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 243\u2013259. Springer, Heidelberg (2011)"},{"issue":"3","key":"8_CR9","first-page":"1","volume":"6","author":"K Chatterjee","year":"2010","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Expressiveness and closure properties for quantitative languages. Logical Methods Comput. Sci. 6(3), 1\u201323 (2010)","journal-title":"Logical Methods Comput. Sci."},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: LICS 2005, pp. 178\u2013187. IEEE Computer Society (2005)","DOI":"10.1109\/LICS.2005.26"},{"key":"8_CR11","unstructured":"Cheung, L., Stoelinga, M., Vaandrager, F.W.: A testing scenario for probabilistic processes. J. ACM 54(6) (2007). Article No. 29"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: Discounting the future in systems theory. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.), ICALP 2003, volume 2719 of LNCS, pp. 1022\u20131037. Springer (2003)","DOI":"10.1007\/3-540-45061-0_79"},{"issue":"37","key":"8_CR13","doi-asserted-by":"publisher","first-page":"3481","DOI":"10.1016\/j.tcs.2009.03.029","volume":"410","author":"M Droste","year":"2009","unstructured":"Droste, M., Rahonis, G.: Weighted automata and weighted logics with discounting. Theor. Comput. Sci. 410(37), 3481\u20133494 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"8_CR14","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1016\/j.entcs.2008.11.019","volume":"220","author":"M Faella","year":"2008","unstructured":"Faella, M., Legay, A., Stoelinga, M.: Model checking quantitative linear time logic. Electr. Notes Theor. Comput. Sci. 220(3), 61\u201377 (2008)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"5","key":"8_CR15","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Formal Asp. Comput."},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31\u201344. Springer, Heidelberg (2006)"},{"issue":"2","key":"8_CR17","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM 47(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"key":"8_CR18","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1016\/0304-3975(84)90049-5","volume":"32","author":"S Miyano","year":"1984","unstructured":"Miyano, S., Hayashi, T.: Alternating finite automata on omega-words. Theor. Comput. Sci. 32, 321\u2013330 (1984)","journal-title":"Theor. Comput. Sci."},{"key":"8_CR19","unstructured":"Nakagawa, S., Hasuo, I.: Near-optimal scheduling for LTL with future discounting (2015). CoRR, abs\/1410.4950"},{"key":"8_CR20","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texas, USA, January 11\u201313, 1989, pp. 179\u2013190. ACM Press (1989)"},{"issue":"2","key":"8_CR21","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1016\/j.fss.2004.12.003","volume":"153","author":"G Rahonis","year":"2005","unstructured":"Rahonis, G.: Infinite fuzzy computations. Fuzzy Sets Syst. 153(2), 275\u2013288 (2005)","journal-title":"Fuzzy Sets Syst."},{"key":"8_CR22","unstructured":"van Glabbeek, R.J.: The linear time-branching time spectrum I; the semantics of concrete, sequential processes. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.), Handbook of Process Algebra, chapter 1, pp. 3\u201399. Elsevier (2001)"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Logics for Concurrency: Structure Versus Automata, vol. 1043 of LNCS, pp. 238\u2013266. Springer-Verlag (1996)","DOI":"10.1007\/3-540-60915-6_6"}],"container-title":["Lecture Notes in Computer Science","Trustworthy Global Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-28766-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T00:57:00Z","timestamp":1748739420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-28766-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319287652","9783319287669"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-28766-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"5 January 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}