{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,14]],"date-time":"2025-04-14T14:27:15Z","timestamp":1744640835143},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040801"},{"type":"electronic","value":"9783642040818"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04081-8_28","type":"book-chapter","created":{"date-parts":[[2009,8,31]],"date-time":"2009-08-31T12:27:08Z","timestamp":1251721628000},"page":"415-430","source":"Crossref","is-referenced-by-count":14,"title":["Concavely-Priced Probabilistic Timed Automata"],"prefix":"10.1007","author":[{"given":"Marcin","family":"Jurdzi\u0144ski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashutosh","family":"Trivedi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"28_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science\u00a0126 (1994)","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-45351-2_8","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2001","unstructured":"Alur, R., La Torre, S., Pappas, G.: Optimal paths in weighted timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol.\u00a02034, p. 49. Springer, Heidelberg (2001)"},{"key":"28_CR3","doi-asserted-by":"crossref","unstructured":"Beauquier, D.: Probabilistic timed automata. Theoretical Computer Science\u00a0292(1) (2003)","DOI":"10.1016\/S0304-3975(01)00215-8"},{"key":"28_CR4","volume-title":"Proc. CDC 2001","author":"G. Behrmann","year":"2001","unstructured":"Behrmann, G., David, A., Larsen, K., M\u00f6ller, O., Pettersson, P., Yi, W.: Uppaal - present and future. In: Proc. CDC 2001, vol.\u00a03. IEEE, Los Alamitos (2001)"},{"key":"28_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"128","DOI":"10.1007\/978-3-642-02017-9_16","volume-title":"TAMC 2009","author":"J. Berendsen","year":"2009","unstructured":"Berendsen, J., Chen, T., Jansen, D.: Undecidability of cost-bounded reachability in priced probabilistic timed automata. In: Chen, T., Cooper, S.B. (eds.) TAMC 2009. LNCS, vol.\u00a05532, pp. 128\u2013137. Springer, Heidelberg (2009)"},{"key":"28_CR6","volume-title":"Proc. QEST 2006","author":"J. Berendsen","year":"2006","unstructured":"Berendsen, J., Jansen, D., Katoen, J.-P.: Probably on time and within budget - on reachability in priced probabilistic timed automata. In: Proc. QEST 2006. IEEE, Los Alamitos (2006)"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Brinksma, E., Larsen, K.: Optimal infinite scheduling for multi-priced timed automata. Formal Methods in System Design\u00a032(1) (2008)","DOI":"10.1007\/s10703-007-0043-4"},{"key":"28_CR8","doi-asserted-by":"crossref","unstructured":"Boyd, S., Vandenberghe, L.: Convex Optimization. CUP, Cambridge (2004)","DOI":"10.1017\/CBO9780511804441"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/3-540-48320-9_7","volume-title":"CONCUR\u201999. Concurrency Theory","author":"L. Alfaro de","year":"1999","unstructured":"de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, p. 66. Springer, Heidelberg (1999)"},{"key":"28_CR10","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-6746-2","volume-title":"Controlled Markov Processes","author":"E. Dynkin","year":"1979","unstructured":"Dynkin, E., Yushkevich, A.: Controlled Markov Processes. Springer, Heidelberg (1979)"},{"key":"28_CR11","doi-asserted-by":"crossref","unstructured":"Falk, J., Horowitz, J.: Critical path problems with concave cost-time curves. Management Science\u00a019(4) (1972)","DOI":"10.1287\/mnsc.19.4.446"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Feng, Y., Xiao, B.: A Continuous-Time Yield Management Model with Multiple Prices and Reversible Price Changes. Management Science\u00a046(5) (2000)","DOI":"10.1287\/mnsc.46.5.644.12050"},{"key":"28_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/3-540-55719-9_103","volume-title":"Automata, Languages and Programming","author":"T. Henzinger","year":"1992","unstructured":"Henzinger, T., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol.\u00a0623, pp. 545\u2013558. Springer, Heidelberg (1992)"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"28_CR15","unstructured":"Jensen, H.: Model checking probabilistic real time systems. In: Proc. 7th Nordic Workshop on Programming Theory, Report 86, pp. 247\u2013261. Chalmers University of Technology (1996)"},{"key":"28_CR16","doi-asserted-by":"crossref","unstructured":"Jurdzinski, M., Kwiatkowska, M., Norman, G., Trivedi, A.: Concavely-priced probabilistic timed automata. Technical Report RR-09-06. Oxford University Computing Laboratory (2009)","DOI":"10.1007\/978-3-642-04081-8_28"},{"key":"28_CR17","doi-asserted-by":"crossref","unstructured":"Jurdzi\u0144ski, M., Sproston, J., Laroussinie, F.: Model checking probabilistic timed automata with one or two clocks. Logical Methods in Computer Science\u00a04(3) (2008)","DOI":"10.2168\/LMCS-4(3:12)2008"},{"key":"28_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-85778-5_5","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"M. Jurdzi\u0144ski","year":"2008","unstructured":"Jurdzi\u0144ski, M., Trivedi, A.: Concavely-priced timed automata. In: Cassez, F., Jard, C. (eds.) FORMATS 2008. LNCS, vol.\u00a05215, pp. 48\u201362. Springer, Heidelberg (2008)"},{"key":"28_CR19","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods in System Design\u00a029 (2006)","DOI":"10.1007\/s10703-006-0005-2"},{"key":"28_CR20","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science\u00a0282 (2002)","DOI":"10.1016\/S0304-3975(01)00046-9"},{"key":"28_CR21","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J., Wang, F.: Symbolic model checking for probabilistic timed automata. Information and Computation\u00a0205(7) (2007)","DOI":"10.1016\/j.ic.2007.01.004"},{"key":"28_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-540-28644-8_25","volume-title":"CONCUR 2004 - Concurrency Theory","author":"F. Laroussinie","year":"2004","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Model checking timed automata with one or two clocks. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 387\u2013401. Springer, Heidelberg (2004)"},{"key":"28_CR23","doi-asserted-by":"crossref","unstructured":"Laroussinie, F., Sproston, J.: State explosion in almost-sure probabilistic reachability. Information Processing Letters\u00a0102(6) (2007)","DOI":"10.1016\/j.ipl.2007.01.003"},{"key":"28_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume-title":"Computer Aided Verification","author":"K. Larsen","year":"2001","unstructured":"Larsen, K., Behrmann, G., Brinksma, E., Fehnker, A., Hune, T., Pettersson, P., Romijn, J.: As cheap as possible: Efficient cost-optimal reachability for priced timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 493. Springer, Heidelberg (2001)"},{"key":"28_CR25","doi-asserted-by":"crossref","unstructured":"Larsen, K., Rasmussen, J.: Optimal reachability for multi-priced timed automata. Theoretical Computer Science\u00a0390(2-3) (2008)","DOI":"10.1016\/j.tcs.2007.09.021"},{"key":"28_CR26","doi-asserted-by":"crossref","unstructured":"Papadimitriou, C., Tsitsiklis, J.: The complexity of Markov decision processes. Mathematics of Operations Research\u00a012 (1987)","DOI":"10.1287\/moor.12.3.441"},{"key":"28_CR27","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M. Puterman","year":"1994","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, Chichester (1994)"},{"key":"28_CR28","doi-asserted-by":"crossref","unstructured":"Torres, E., Dominguez, J., Valdes, L., Aza, R.: Passenger waiting time in an airport and expenditure carried out in the commercial area. Journal of Air Transport Management\u00a011(6) (2005)","DOI":"10.1016\/j.jairtraman.2005.04.001"},{"key":"28_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-48778-6_18","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"S. Tripakis","year":"1999","unstructured":"Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol.\u00a01601, p. 299. Springer, Heidelberg (1999)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2009 - Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04081-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T04:47:20Z","timestamp":1558500440000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04081-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040801","9783642040818"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04081-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}