{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T17:22:57Z","timestamp":1725988977445},"publisher-location":"Cham","reference-count":27,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030002435"},{"type":"electronic","value":"9783030002442"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-030-00244-2_18","type":"book-chapter","created":{"date-parts":[[2018,8,30]],"date-time":"2018-08-30T00:12:38Z","timestamp":1535587958000},"page":"269-283","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP"],"prefix":"10.1007","author":[{"given":"Iulian","family":"Ober","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,30]]},"reference":[{"issue":"2","key":"18_CR1","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":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/3-540-36135-9_16","volume-title":"Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002","author":"G Audemard","year":"2002","unstructured":"Audemard, G., Cimatti, A., Kornilowicz, A., Sebastiani, R.: Bounded model checking for timed systems. In: Peled, D.A., Vardi, M.Y. (eds.) FORTE 2002. LNCS, vol. 2529, pp. 243\u2013259. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36135-9_16"},{"issue":"2","key":"18_CR3","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1002\/spe.1006","volume":"41","author":"G Behrmann","year":"2011","unstructured":"Behrmann, G., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Developing UPPAAL over 15 years. Softw. Pract. Exper. 41(2), 133\u2013142 (2011)","journal-title":"Softw. Pract. Exper."},{"key":"18_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/BFb0055643","volume-title":"CONCUR 1998 Concurrency Theory","author":"J Bengtsson","year":"1998","unstructured":"Bengtsson, J., Jonsson, B., Lilius, J., Yi, W.: Partial order reductions for timed systems. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 485\u2013500. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055643"},{"key":"18_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Bouyer, P.: Weighted timed automata: model-checking and games. Electron. Notes Theor. Comput. Sci. 158, 3\u201317 (2006). Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics (MFPS XXII)","DOI":"10.1016\/j.entcs.2006.04.002"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-48213-X_14","volume-title":"SDL 2001: Meeting UML","author":"M Bozga","year":"2001","unstructured":"Bozga, M., Graf, S., Mounier, L., Ober, I., Roux, J.-L., Vincent, D.: Timed extensions for SDL. In: Reed, R., Reed, J. (eds.) SDL 2001. LNCS, vol. 2078, pp. 223\u2013240. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-48213-X_14"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/978-3-540-30080-9_8","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"M Bozga","year":"2004","unstructured":"Bozga, M., Graf, S., Ober, I., Ober, I., Sifakis, J.: The IF toolset. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 237\u2013267. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30080-9_8"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-642-13464-7_13","volume-title":"Formal Techniques for Distributed Systems","author":"L Bu","year":"2010","unstructured":"Bu, L., Cimatti, A., Li, X., Mover, S., Tonetta, S.: Model checking of hybrid systems using shallow synchronization. In: Hatcliff, J., Zucca, E. (eds.) FMOODS\/FORTE -2010. LNCS, vol. 6117, pp. 155\u2013169. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-13464-7_13"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45739-9","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","year":"2002","unstructured":"Damm, W., Olderog, E.-R. (eds.): FTRTFT 2002. LNCS, vol. 2469. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45739-9"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/3-540-45923-5_15","volume-title":"Fundamental Approaches to Software Engineering","author":"A David","year":"2002","unstructured":"David, A., M\u00f6ller, M.O., Yi, W.: Formal verification of UML statecharts with real-time extensions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 218\u2013232. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45923-5_15"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"DL Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 197\u2013212. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_17"},{"key":"18_CR13","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1016\/j.entcs.2004.08.061","volume":"133","author":"M Fr\u00e4nzle","year":"2005","unstructured":"Fr\u00e4nzle, M., Herde, C.: Efficient proof engines for bounded model checking of hybrid systems. Electron. Notes Theor. Comput. Sci. 133, 119\u2013137 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/3-540-36573-7_3","volume-title":"Telecommunications and beyond: The BroaderApplicability of SDL and MSC","author":"S Graf","year":"2003","unstructured":"Graf, S.: Expression of time and duration constraints in SDL. In: Sherratt, E. (ed.) SAM 2002. LNCS, vol. 2599, pp. 38\u201352. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36573-7_3"},{"issue":"2","key":"18_CR15","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/s10270-007-0077-5","volume":"7","author":"S Graf","year":"2008","unstructured":"Graf, S.: OMEGA: correct development of real time and embedded systems. Softw. Syst. Model. 7(2), 127\u2013130 (2008)","journal-title":"Softw. Syst. Model."},{"key":"18_CR16","unstructured":"Gurobi Optimization Inc., Reference manual v. 7.5. https:\/\/www.gurobi.com\/documentation\/7.5\/refman.pdf . Accessed on 8 June 2018"},{"key":"18_CR17","doi-asserted-by":"crossref","unstructured":"Knapp, A., Merz, S., Rauh, C.: Model checking - timed UML state machines and collaborations. In: Damm and Olderog [10], pp. 395\u2013416","DOI":"10.1007\/3-540-45739-9_23"},{"key":"18_CR18","first-page":"271","volume":"6","author":"KG Larsen","year":"1999","unstructured":"Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Clock difference diagrams. Nord. J. Comput. 6, 271\u2013298 (1999)","journal-title":"Clock difference diagrams. Nord. J. Comput."},{"issue":"1","key":"18_CR19","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.tcs.2005.07.023","volume":"345","author":"D Lugiez","year":"2005","unstructured":"Lugiez, D., Niebert, P., Zennou, S.: A partial order semantics approach to the clock explosion problem of timed automata. Theor. Comput. Sci. 345(1), 27\u201359 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/978-3-642-12002-2_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Malinowski","year":"2010","unstructured":"Malinowski, J., Niebert, P.: SAT based bounded model checking with partial order semantics for timed automata. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 405\u2013419. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_34"},{"key":"18_CR21","unstructured":"MathSAT 5. http:\/\/mathsat.fbk.eu . Accessed 8 June 2018"},{"key":"18_CR22","unstructured":"M\u00f6ller, O.: CSMA\/CD protocol specification (UPPAAL benchmark). https:\/\/www.it.uu.se\/research\/group\/darts\/uppaal\/benchmarks\/#CSMA . Accessed 8 June 2018"},{"key":"18_CR23","doi-asserted-by":"publisher","DOI":"10.1002\/9781118627372","volume-title":"Integer and Combinatorial Optimization","author":"GL Nemhauser","year":"1988","unstructured":"Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley-Interscience, New York (1988)"},{"key":"18_CR24","doi-asserted-by":"crossref","unstructured":"Niebert, P., Mahfoudh, M., Asarin, E., Bozga, M., Maler, O., Jain, N.: Verification of timed automata via satisfiability checking. In: Damm and Olderog [10], pp. 225\u2013244","DOI":"10.1007\/3-540-45739-9_15"},{"key":"18_CR25","doi-asserted-by":"crossref","unstructured":"M. Sorea. Bounded model checking for timed automata. Electron. Notes Theor. Comput. Sci. 68(5), 116\u2013134 (2003). MTCS 2002, Models for Time-Critical Systems (CONCUR 2002 Satellite Workshop)","DOI":"10.1016\/S1571-0661(04)80523-1"},{"issue":"1","key":"18_CR26","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s10009-003-0135-4","volume":"6","author":"F Wang","year":"2004","unstructured":"Wang, F.: Efficient verification of timed automata with BDD-like data structures. STTT 6(1), 77\u201397 (2004)","journal-title":"STTT"},{"issue":"1\u20132","key":"18_CR27","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/s100090050009","volume":"1","author":"S Yovine","year":"1997","unstructured":"Yovine, S.: KRONOS: A verification tool for real-time systems. STTT 1(1\u20132), 123\u2013133 (1997)","journal-title":"STTT"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-00244-2_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,23]],"date-time":"2019-10-23T02:02:59Z","timestamp":1571796179000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-00244-2_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783030002435","9783030002442"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-00244-2_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}