{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,2]],"date-time":"2026-05-02T02:46:45Z","timestamp":1777690005787,"version":"3.51.4"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2016,10,13]],"date-time":"2016-10-13T00:00:00Z","timestamp":1476316800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["ZI 1516\/1-1"],"award-info":[{"award-number":["ZI 1516\/1-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2018,3]]},"DOI":"10.1007\/s00236-016-0279-9","type":"journal-article","created":{"date-parts":[[2016,10,13]],"date-time":"2016-10-13T11:11:11Z","timestamp":1476357071000},"page":"129-152","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Parameterized linear temporal logics meet costs: still not costlier than LTL"],"prefix":"10.1007","volume":"55","author":[{"given":"Martin","family":"Zimmermann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,13]]},"reference":[{"issue":"3","key":"279_CR1","doi-asserted-by":"crossref","first-page":"388","DOI":"10.1145\/377978.377990","volume":"2","author":"R Alur","year":"2001","unstructured":"Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for \u201cmodel measuring\u201d. ACM Trans. Comput. Log. 2(3), 388\u2013407 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"279_CR2","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Babai, L. (ed.) STOC 04, pp. 202\u2013211. ACM (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"279_CR3","doi-asserted-by":"crossref","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, vol. 5643 of LNCS, pp. 140\u2013156. Springer (2009)","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"279_CR4","doi-asserted-by":"crossref","unstructured":"Boom, M.V.: Weak cost monadic logic over infinite trees. In: Murlak, F., Sankowski, P. (eds.) MFCS 2011, vol. 6907 of LNCS, pp. 580\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22993-0_52"},{"key":"279_CR5","doi-asserted-by":"crossref","unstructured":"Boja\u0144czyk, M.: A bounding quantifier. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004, vol. 3210 of LNCS, pp. 41\u201355. Springer (2004)","DOI":"10.1007\/978-3-540-30124-0_7"},{"issue":"3","key":"279_CR6","doi-asserted-by":"crossref","first-page":"554","DOI":"10.1007\/s00224-010-9279-2","volume":"48","author":"M Boja\u0144czyk","year":"2011","unstructured":"Boja\u0144czyk, M.: Weak MSO with the unbounding quantifier. Theory Comput. Syst. 48(3), 554\u2013576 (2011)","journal-title":"Theory Comput. Syst."},{"key":"279_CR7","doi-asserted-by":"crossref","unstructured":"Bojanczyk, M.: Weak MSO + U with path quantifiers over infinite trees. In: Esparza, J., Fraigniaud, P., Husfeldt, T., Koutsoupias, E. (eds.) ICALP 2014 Part II, vol. 8573 of LNCS, pp. 38\u201349. Springer (2014)","DOI":"10.1007\/978-3-662-43951-7_4"},{"key":"279_CR8","unstructured":"Boja\u0144czyk, M., Colcombet, T.: Bounds in $$\\omega $$ \u03c9 -regularity. In: LICS 2006, pp. 285\u2013296. IEEE Computer Society (2006)"},{"key":"279_CR9","unstructured":"Boja\u0144czyk, M., Toru\u0144czyk, S.: Weak MSO + U over infinite trees. In: D\u00fcrr, C., Wilke, T. (eds.) STACS 2012, vol.\u00a014 of LIPIcs, pp. 648\u2013660. Schloss Dagstuhl\u2013Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"279_CR10","doi-asserted-by":"crossref","unstructured":"Bozzelli, L.: Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007, vol. 4703 of LNCS, pp. 476\u2013491. Springer (2007)","DOI":"10.1007\/978-3-540-74407-8_32"},{"key":"279_CR11","doi-asserted-by":"crossref","unstructured":"Bozzelli, L., S\u00e1nchez, C.: Visibly linear temporal logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014, vol. 8562 of LNCS, pp. 418\u2013483. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_33"},{"issue":"1","key":"279_CR12","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1007\/s00236-013-0190-6","volume":"51","author":"L Bozzelli","year":"2014","unstructured":"Bozzelli, L., S\u00e1nchez, C.: Visibly rational expressions. Acta Inform. 51(1), 25\u201349 (2014)","journal-title":"Acta Inform."},{"key":"279_CR13","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Kucera, A., Novotn\u00fd, P.: Efficient controller synthesis for consumption games with multiple resource types. In: Madhusudan, P., Seshia, Sanjit\u00a0A. (eds.) CAV 2012, vol. 7358 of LNCS, pp. 23\u201338. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_8"},{"key":"279_CR14","doi-asserted-by":"crossref","unstructured":"C\u0306ern\u00fd, P., Chatterjee, K., Henzinger, T.A., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011, vol. 6806 of LNCS, pp. 243\u2013259. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_20"},{"key":"279_CR15","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L.: Energy parity games. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der H., Friedhelm, S., Paul\u00a0G. (eds.) ICALP 2010 Part II, vol. 6199 of LNCS, pp. 599\u2013610. Springer (2010)","DOI":"10.1007\/978-3-642-14162-1_50"},{"key":"279_CR16","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Horn, F.: Finitary winning in omega-regular games. ACM Trans. Comput. Log., 11(1) (2009)","DOI":"10.1145\/1614431.1614432"},{"key":"279_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Jurdzi\u0144ski, M.: Mean-payoff parity games. In: LICS 2005, pp. 178\u2013187. IEEE Computer Society (2005)","DOI":"10.1109\/LICS.2005.26"},{"key":"279_CR18","doi-asserted-by":"crossref","unstructured":"Colcombet, T.: The theory of stabilisation monoids and regular cost functions. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S.E., Thomas, W. (eds.) ICALP 2009 Part II, vol. 5556 of LNCS, pp. 139\u2013150. Springer (2009)","DOI":"10.1007\/978-3-642-02930-1_12"},{"key":"279_CR19","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (eds.) IJCAI. IJCAI\/AAAI (2013)"},{"key":"279_CR20","doi-asserted-by":"crossref","unstructured":"Faymonville, P., Zimmermann, M.: Parametric linear dynamic logic. In: Peron, A., Piazza, C. (eds.) GandALF 2014, vol. 161 of EPTCS, pp. 60\u201373 (2014)","DOI":"10.4204\/EPTCS.161.8"},{"key":"279_CR21","unstructured":"Faymonville, P., Zimmermann, M.: Parametric linear dynamic logic (full version). arXiv:1504.03880 (2015). Accepted for publication in information and computation"},{"key":"279_CR22","doi-asserted-by":"crossref","unstructured":"Fijalkow, N., Zimmermann, M.: Parity and Streett games with costs. LMCS, 10(2) (2014)","DOI":"10.2168\/LMCS-10(2:14)2014"},{"key":"279_CR23","unstructured":"Kamp, H.W.: Tense Logic and the Theory of Linear Order. PhD thesis, Computer Science Department, University of California at Los\u00a0Angeles, USA (1968)"},{"issue":"2","key":"279_CR24","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1007\/s10703-009-0067-z","volume":"34","author":"O Kupferman","year":"2009","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: From liveness to promptness. Form. Methods Syst. Des. 34(2), 83\u2013103 (2009)","journal-title":"Form. Methods Syst. Des."},{"key":"279_CR25","doi-asserted-by":"crossref","unstructured":"Leucker, M., S\u00e1nchez, C.: Regular linear temporal logic. In: Jones, C., Liu, Z., Woodcock, J. (eds.) ICTAC 2007, vol. 4711 of LNCS, pp. 291\u2013305. Springer (2007)","DOI":"10.1007\/978-3-540-75292-9_20"},{"key":"279_CR26","doi-asserted-by":"crossref","unstructured":"Mogavero, F., Murano, A., Sorrentino, L.: On promptness in parity games. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) LPAR 2013, vol. 8312 of LNCS, pp. 601\u2013618. Springer (2013)","DOI":"10.1007\/978-3-642-45221-5_40"},{"key":"279_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"279_CR28","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"279_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Ronchi\u00a0Della Rocca, S. (eds.) ICALP 1989, vol. 372 of LNCS, pp. 652\u2013671. Springer (1989)","DOI":"10.1007\/BFb0035790"},{"key":"279_CR30","doi-asserted-by":"crossref","unstructured":"Schewe, S.: Solving parity games in big steps. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007, vol. 4855 of LNCS, pp. 449\u2013460. Springer (2007)","DOI":"10.1007\/978-3-540-77050-3_37"},{"issue":"3","key":"279_CR31","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM 32(3), 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"279_CR32","unstructured":"Tentrup, L., Weinert, A., Zimmermann, M.: Approximating optimal bounds in Prompt-LTL realizability in doubly-exponential time (2015). arXiv:1511.09450"},{"key":"279_CR33","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: A temporal fixpoint calculus. In: Ferrante, J., Mager, P. (eds.) POPL 88, pp. 250\u2013259. ACM Press (1988)","DOI":"10.1145\/73560.73582"},{"key":"279_CR34","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: The rise and fall of LTL. In: D\u2019Agostino, G., Torre, S.L. (eds.) GandALF 2011, vol. 54 of EPTCS (2011)","DOI":"10.4204\/EPTCS.54.0.2"},{"issue":"1","key":"279_CR35","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"279_CR36","unstructured":"Weinert, A., Zimmermann, M.: Visibly linear dynamic logic (2015). arXiv:1512.05177"},{"issue":"1\u20132","key":"279_CR37","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1\u20132), 72\u201399 (1983)","journal-title":"Inf. Control"},{"key":"279_CR38","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1016\/j.tcs.2012.07.039","volume":"493","author":"M Zimmermann","year":"2013","unstructured":"Zimmermann, M.: Optimal bounds in parametric LTL games. Theor. Comput. Sci. 493, 30\u201345 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"279_CR39","doi-asserted-by":"crossref","unstructured":"Zimmermann, M.: Parameterized linear temporal logics meet costs: still not costlier than LTL. In: Esparza, J., Tronci, E. (eds.) GandALF 2015, vol. 193 of EPTCS, pp. 144\u2013157 (2015)","DOI":"10.4204\/EPTCS.193.11"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0279-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0279-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0279-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,11]],"date-time":"2025-06-11T10:13:16Z","timestamp":1749636796000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0279-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,10,13]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,3]]}},"alternative-id":["279"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0279-9","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,10,13]]}}}