{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T17:09:37Z","timestamp":1769360977643,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540401179","type":"print"},{"value":"9783540448297","type":"electronic"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/3-540-44829-2_1","type":"book-chapter","created":{"date-parts":[[2007,7,3]],"date-time":"2007-07-03T16:01:40Z","timestamp":1183478500000},"page":"1-17","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Optimal Scheduling Using Branch and Bound with SPIN 4.0"],"prefix":"10.1007","author":[{"given":"Theo C.","family":"Ruys","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,4,15]]},"reference":[{"key":"1_CR1","unstructured":"Advanced Methods for Timed Systems (AMETIST) Project. IST-2001-35304. Homepage: http:\/\/ametist.cs.utwente.nl\/."},{"key":"1_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/3-540-45319-9_13","volume-title":"Procs. of the 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001)","author":"G. Behrmann","year":"2001","unstructured":"G. Behrmann, A. Fehnker, T. Hune, K. Larsen, P. Pettersson, and J. Romijn. Efficient Guiding Towards Cost-Optimality in Uppaal. In T. Margaria and W. Yi, editors, Procs. of the 7th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), volume 2031 of LNCS, pages 174\u2013188, Genova, Italy, April 2001. Springer."},{"key":"1_CR3","unstructured":"O. S. Benli. The Branch-and-Bound Approach. In Anil Mital, editor, Industrial Engineering Applications and Practice: Users\u2019 Encyclopedia, 1999. CD-ROM edition, chapter available from http:\/\/http:\/\/www.csulb.edu\/~obenli\/."},{"key":"1_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10722468_1","volume-title":"SPIN Model Checking and Software Verification, Procs. of the 7th Int. SPIN Workshop (SPIN\u20192000)","author":"D. Bo\u0161na\u010dki","year":"2000","unstructured":"D. Bo\u0161na\u010dki, D. Dams, and L. Holenderski. Symmetric Spin. In Havelund et al. [9], pages 1\u201319."},{"key":"1_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/10722468_5","volume-title":"SPIN Model Checking and Software Verification, Procs. of the 7th Int. SPIN Workshop (SPIN\u20192000)","author":"E. Brinksma","year":"2000","unstructured":"E. Brinksma and A. Mader. Verification and Optimization of a PLC Control Schedule. In Havelund et al. [9], pages 73\u201392."},{"key":"1_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"Model Checking Software, Procs. of the 8th Int. SPIN Workshop","author":"S. Edelkamp","year":"2001","unstructured":"S. Edelkamp, A. L. Lafuente, and S. Leue. Directed Explicit Model Checking with HSF-SPIN. In M. B. Dwyer, editor, Model Checking Software, Procs. of the 8th Int. SPIN Workshop, volume 2057 of LNCS, pages 57\u201379, Toronto, Canada, May 2001. Springer."},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"A. Fehnker. Scheduling a Steel Plant with Timed Automata. In Procs. of the 6th Int. Conf. on Real-Time Computing Systems and Applications (RTCSA 1999), pages 280\u2013286. IEEE Computer Society, 1999.","DOI":"10.1109\/RTCSA.1999.811256"},{"key":"1_CR8","volume-title":"Citius Vilius Melius \u2014 Guiding and Cost-Optimality in Model Checking of Timed and Hybrid Systems","author":"A. Fehnker","year":"2002","unstructured":"A. Fehnker. Citius Vilius Melius \u2014 Guiding and Cost-Optimality in Model Checking of Timed and Hybrid Systems. PhD thesis, University of Nijmegen, The Netherlands, April 2002."},{"key":"1_CR9","series-title":"Lect Notes Comput Sci","volume-title":"SPIN Model Checking and Software Verification, Procs. of the 7th Int. SPIN Workshop (SPIN\u20192000)","year":"2000","unstructured":"K. Havelund, J. Penix, and W. Visser, editors. SPIN Model Checking and Software Verification, Procs. of the 7th Int. SPIN Workshop (SPIN\u20192000), volume 1885 of LNCS, Stanford, California, USA, August 2000. Springer."},{"key":"1_CR10","volume-title":"The SPIN Model Checker \u2014 Primer and Reference Manual","author":"G. J. Holzman","year":"2003","unstructured":"G. J. Holzman. The SPIN Model Checker \u2014 Primer and Reference Manual. Addison-Wesley, Boston, USA, 2003."},{"key":"1_CR11","unstructured":"G. J. Holzmann. Spin homepage: http:\/\/spinroot.com\/."},{"key":"1_CR12","volume-title":"Design and Validation of Computer Protocols","author":"G. J. Holzmann","year":"1991","unstructured":"G. J. Holzmann. Design and Validation of Computer Protocols. Prentice Hall, Englewood Cliffs, New Jersey, USA, 1991."},{"issue":"5","key":"1_CR13","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. J. Holzmann","year":"1997","unstructured":"G. J. Holzmann. The Model Checker Spin. IEEE Transactions on Software Engineering, 23(5):279\u2013295, May 1997.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"1_CR14","series-title":"DIMACS Series","volume-title":"The SPIN Verification System, Procs. of the 2nd Int. SPIN Workshop (SPIN\u201996)","author":"G. J. Holzmann","year":"1996","unstructured":"G. J. Holzmann, D. Peled, and M. Yannakakis. On Nested Depth First Search. In J.-C. Gr\u2019egoire, G. J. Holzmann, and D. A. Peled, editors, The SPIN Verification System, Procs. of the 2nd Int. SPIN Workshop (SPIN\u201996), volume 32 of DIMACS Series, Rutgers University, New Jersey, USA, August 1996. AMS."},{"key":"1_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"493","DOI":"10.1007\/3-540-44585-4_47","volume-title":"Procs. of the 13th Int. Conf. on Computer Aided Verification (CAV 2001)","author":"K. Larsen","year":"2001","unstructured":"K. Larsen, G. Behrmann, E. Brinksma, A. Fehnker, T. Hune, P. Pettersson, and J. Romijn. As Cheap As Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata. In G. Berry, H. Comon, and A. Finkel, editors, Procs. of the 13th Int. Conf. on Computer Aided Verification (CAV 2001), volume 2102 of LNCS, pages 493\u2013505, Paris, France, July 2001. Springer."},{"key":"1_CR16","unstructured":"Princeton University, Mathematics Department. Traveling Salesman Problem \u2014 Homepage. http:\/\/www.math.princeton.edu\/tsp\/."},{"key":"1_CR17","series-title":"Lect Notes Comput Sci","volume-title":"The Travelling Salesman \u2014 Computational Solutions for TSP Applications","author":"G. Reinelt","year":"1994","unstructured":"G. Reinelt. The Travelling Salesman \u2014 Computational Solutions for TSP Applications, volume 840 of LNCS. Springer, 1994."},{"key":"1_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/10722468_17","volume-title":"SPIN Model Checking and Software Verification, Procs. of the 7th Int. SPIN Workshop (SPIN\u20192000)","author":"T. C. Ruys","year":"2000","unstructured":"T. C. Ruys. Low-Fat Recipes for Spin. In Havelund et al. [9], pages 287\u2013321."},{"key":"1_CR19","volume-title":"Towards Effective Model Checking","author":"T. C. Ruys","year":"2001","unstructured":"T. C. Ruys. Towards Effective Model Checking. PhD thesis, University of Twente, Enschede, The Netherlands, March 2001. Available from the author\u2019s homepage."},{"key":"1_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/BFb0054185","volume-title":"Procs. of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998)","author":"T. C. Ruys","year":"1998","unstructured":"T. C. Ruys and E. Brinksma. Experience with Literate Programming in the Modelling and Validation of Systems. In B. Steffen, editor, Procs. of the 4th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998), number 1384 in LNCS, pages 393\u2013408, Lisbon, Portugal, April 1998."},{"key":"1_CR21","volume-title":"Regenerative Stochastic Simulation","author":"G. S. Shedler","year":"1993","unstructured":"G. S. Shedler. Regenerative Stochastic Simulation. Academic Press, Boston, 1993."},{"key":"1_CR22","volume-title":"Operations Research \u2014 Applications and Algorithms","author":"W. L. Winston","year":"1994","unstructured":"W. L. Winston. Operations Research \u2014 Applications and Algorithms. Duxbury Press, Belmont, California, USA, third edition, 1994.","edition":"third edition"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44829-2_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,18]],"date-time":"2025-01-18T04:02:36Z","timestamp":1737172956000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-44829-2_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540401179","9783540448297"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44829-2_1","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2003]]},"assertion":[{"value":"15 April 2003","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}