{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,23]],"date-time":"2025-05-23T04:16:03Z","timestamp":1747973763045,"version":"3.41.0"},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319175805"},{"type":"electronic","value":"9783319175812"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-17581-2_5","type":"book-chapter","created":{"date-parts":[[2015,4,15]],"date-time":"2015-04-15T12:22:36Z","timestamp":1429100556000},"page":"62-75","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Checking Integral Real-Time Automata for Extended Linear Duration Invariants"],"prefix":"10.1007","author":[{"given":"Changil","family":"Choe","sequence":"first","affiliation":[]},{"given":"Univan","family":"Ahn","sequence":"additional","affiliation":[]},{"given":"Song","family":"Han","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,4,16]]},"reference":[{"issue":"5","key":"5_CR1","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"Z Chaochen","year":"1991","unstructured":"Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)","journal-title":"Inf. Process. Lett."},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/3-540-58468-4_161","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"C Zhou","year":"1994","unstructured":"Zhou, C.: Linear duration invariants. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 86\u2013109. Springer, Heidelberg (1994)"},{"key":"5_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-57318-6_29","volume-title":"Hybrid Systems","author":"Y Kesten","year":"1993","unstructured":"Kesten, Y., Pnueli, A., Sifakis, J., Yovine, S.: Integration graphs: a class of decidable hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 179\u2013208. Springer, Heidelberg (1993)"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Braberman, V.A., Van Hung, D.: On checking timed automata for linear duration invariants. In: Proceedings of the 19th Real-Time Systems Symposium RTSS 1998, pp. 264\u2013273. IEEE Computer Society Press, Los Alamitos (1998)","DOI":"10.1109\/REAL.1998.739752"},{"key":"5_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/978-3-540-78849-2","volume-title":"ICTAC 2008","author":"M Zhang","year":"2008","unstructured":"Zhang, M., Van Hung, D., Liu, Z.: Verification of linear duration invariants by model checking CTL properties. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 395\u2013409. Springer, Heidelberg (2008)"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-11623-0_14","volume-title":"Fundamentals of Software Engineering","author":"M Zhang","year":"2010","unstructured":"Zhang, M., Liu, Z., Zhan, N.: Model checking linear duration invariants of networks of automata. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 244\u2013259. Springer, Heidelberg (2010)"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/978-3-540-31862-0_22","volume-title":"ICTAC 2004","author":"PH Thai","year":"2005","unstructured":"Thai, P.H., Van Hung, D.: Verifying linear duration constraints of timed automata. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 295\u2013309. Springer, Heidelberg (2005)"},{"issue":"1","key":"5_CR8","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/32.210306","volume":"19","author":"AP Ravn","year":"1993","unstructured":"Ravn, A.P., Rischel, H., Hansen, K.M.: Specifying and verifying requirements of real-time systems. IEEE Trans. Softw. Eng. 19(1), 41\u201355 (1993)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"5_CR9","first-page":"431","volume-title":"A Classical Mind, Essays in Honour of C. A. R. Hoare","author":"Z Chaochen","year":"1994","unstructured":"Chaochen, Z., Xiaoshan, L.: A mean-value duration calculus. In: Roscoe, A.W. (ed.) A Classical Mind, Essays in Honour of C. A. R. Hoare, pp. 431\u2013451. Prentice Hall International, Englewood Cliffs (1994)"},{"issue":"2","key":"5_CR10","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"5_CR11","unstructured":"S$$\\phi $$rensen, E.V., Ravn A.P., Rischel H.: Control Program for a Gas Burner: Part 1: Informal Requirements, ProCoS Case Study 1. ProCoS I, ESPRIT BRA 3104, Report No. ID\/DTH EVS2, Department of Computer Science, Technical University of Denmark, Lyngby (1990)"},{"key":"5_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-57318-6_30","volume-title":"Hybrid Systems","author":"R Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209\u2013229. Springer, Heidelberg (1993)"},{"key":"5_CR13","series-title":"A Formal Approach to Real-Time Systems.","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-06784-0","volume-title":"Duration Calculus","author":"Z Chaochen","year":"2004","unstructured":"Chaochen, Z., Hansen, M.R.: Duration Calculus. A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004)"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"58","DOI":"10.1007\/3-540-56503-5_8","volume-title":"Symposium on Theoretical Aspects of Computer Science (STACS 93)","author":"Z Chaochen","year":"1993","unstructured":"Chaochen, Z., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Finkel, A., Wagner, K.W. (eds.) (STACS 93). LNCS, vol. 665, pp. 58\u201368. Springer-Verlag, Heidelberg (1993)"},{"key":"5_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/3-540-57318-6_23","volume-title":"Hybrid Systems","author":"Z Chaochen","year":"1993","unstructured":"Chaochen, Z., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. LNCS, vol. 736, pp. 36\u201359. Springer, Heidelberg (1993)"},{"key":"5_CR16","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1016\/j.cam.2005.10.034","volume":"197","author":"H Zhang","year":"2006","unstructured":"Zhang, H., Wang, S.: Global optimization of separable objective functions on convex polyhedra via piecewise-linear approximation. J. Comput. Appl. Math. 197, 212\u2013217 (2006)","journal-title":"J. Comput. Appl. Math."},{"key":"5_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/11561163_8","volume-title":"Formal Methods for Components and Objects","author":"G Behrmann","year":"2005","unstructured":"Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Priced timed automata: algorithms and applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 162\u2013182. Springer, Heidelberg (2005)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Bouyer, P.: Weighted timed automata: model-checking and games. In: Brookes, S., Mislove (eds.) Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, vol. 158, pp. 3\u201317 (2006)","DOI":"10.1016\/j.entcs.2006.04.002"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-17581-2_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,22]],"date-time":"2025-05-22T15:36:36Z","timestamp":1747928196000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-17581-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319175805","9783319175812"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-17581-2_5","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"16 April 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}