{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,18]],"date-time":"2025-10-18T20:39:37Z","timestamp":1760819977696},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418658"},{"type":"electronic","value":"9783540453192"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45319-9_13","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:50:47Z","timestamp":1184601047000},"page":"174-188","source":"Crossref","is-referenced-by-count":60,"title":["Efficient Guiding Towards Cost-Optimality in UPPAAL"],"prefix":"10.1007","author":[{"given":"Gerd","family":"Behrmann","sequence":"first","affiliation":[]},{"given":"Ansgar","family":"Fehnker","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Hune","sequence":"additional","affiliation":[]},{"given":"Kim","family":"Larsen","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Pettersson","sequence":"additional","affiliation":[]},{"given":"Judi","family":"Romijn","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"13_CR1","doi-asserted-by":"crossref","unstructured":"D. Applegate and W. Cook. A Computational Study of the Job-Shop Scheduling Problem. OSRA Journal on Computing 3, pages 149\u2013156, 1991.","DOI":"10.1287\/ijoc.3.2.149"},{"key":"13_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"546","DOI":"10.1007\/BFb0028779","volume-title":"Proc. of the 10th Int. Conf. on Computer Aided Verification","author":"M. Bozga","year":"1998","unstructured":"M. Bozga, C. Daws, O. Maler, A. Olivero, S. Tripakis, and S. Yovine. Kronos: A Model-Checking Tool for Real-Time Systems. In Proc. of the 10th Int. Conf. on Computer Aided Verification, number 1427 in Lecture Notes in Computer Science, pages 546\u2013550. Springer-Verlag, 1998."},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"G. Behrmann, A. Fehnker, T. Hune, K. G. Larsen, P. Pettersson, J. Romijn, and F. Vaandrager. Minimum-Cost Reachability for Priced Timed Automata. Accepted for Hybrid Systems: Computation and Control, 2001.","DOI":"10.1007\/3-540-45351-2_15"},{"key":"13_CR4","unstructured":"P. Brucker, B. Jurisch, and B. Sievers. Code of a Branch & Bound Algorithm for the Job Shop Problem. Available at url http:\/\/www.mathematik.uni-osnabrueck.de\/research\/OR\/ ,1995."},{"key":"13_CR5","unstructured":"R. Boel and G. Stremersch. Report for VHS: Timed Petri Net Model of Steel Plant at SIDMAR. Technical report, SYSTeMS Group, University Ghent, 1999."},{"key":"13_CR6","series-title":"Lect Notes Comput Sci","first-page":"197","volume-title":"Proc. of Automatic Verification Methods for Finite State Systems","author":"D. Dill","year":"1989","unstructured":"D. Dill. Timing Assumptions and Verification of Finite-State Concurrent Systems. In J. Sifakis, editor, Proc. of Automatic Verification Methods for Finite State Systems, number 407 in Lecture Notes in Computer Science, pages 197\u2013212. Springer-Verlag, 1989."},{"key":"13_CR7","unstructured":"A. Fehnker. Bounding and heuristics in forward reachability algorithms. Technical Report CSI-R0002, Computing Science Institute Nijmegen, 1999."},{"key":"13_CR8","doi-asserted-by":"crossref","unstructured":"A. Fehnker. Scheduling a steel plant with timed automata. In Proceedings of the 6th International Conference on Real-Time Computing Systems and Applications (RTCSA99), pages 280\u2013286. IEEE Computer Society, 1999.","DOI":"10.1109\/RTCSA.1999.811256"},{"key":"13_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"460","DOI":"10.1007\/3-540-63166-6_48","volume-title":"Proc. of the 9th Int. Conf. on Computer Aided Verification","author":"T. A. Henzinger","year":"1997","unstructured":"T. A. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: A Model Checker for Hybird Systems. In Orna Grumberg, editor, Proc. of the 9th Int. Conf. on Computer Aided Verification, number 1254 in Lecture Notes in Computer Science, pages 460\u2013463. Springer-Verlag, 1997."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"T. Hune, K. G. Larsen, and P. Pettersson. Guided synthesis of control programs using UPPAAL for VHS case study 5. VHS deliverable, 1999.","DOI":"10.7146\/brics.v7i37.20203"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"T. Hune, K. G. Larsen, and P. Pettersson. Guided Synthesis of Control Programs Using Uppaal. In Ten H. Lai, editor, Proc. of the IEEE ICDCS International Workshop on Distributed Systems Verification and Validation, pages E15\u2013E22. IEEE Computer Society Press, April 2000.","DOI":"10.7146\/brics.v7i37.20203"},{"key":"13_CR12","series-title":"Lect Notes Comput Sci","first-page":"575","volume-title":"Proc. of Workshop on Verification and Control of Hybrid Systems III","author":"K. G. Larsen","year":"1995","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Diagnostic Model-Checking for Real-Time Systems. In Proc. of Workshop on Verification and Control of Hybrid Systems III, number 1066 in Lecture Notes in Computer Science, pages 575\u2013586. Springer-Verlag, October 1995."},{"issue":"1\u20132","key":"13_CR13","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K. G. Larsen","year":"1997","unstructured":"K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a Nutshell. Int. Journal on Software Tools for Technology Transfer, 1(1\u20132):134\u2013152, October 1997.","journal-title":"Int. Journal on Software Tools for Technology Transfer"},{"key":"13_CR14","unstructured":"P. Niebert, S. Tripakis, and S. Yovine. Minimum-time reachability for timed automata. In IEEE Mediteranean Control Conference, 2000. Accepted for publication."},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"P. Niebert and S. Yovine. Computing optimal operation schemes for multi batch operation of chemical plants. VHS deliverable, May 1999. Draft.","DOI":"10.1007\/3-540-46430-1_29"},{"key":"13_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/BFb0054185","volume-title":"Proceedings of the Fourth International Conference 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 Bernhard Steffen, editor, Proceedings of the Fourth International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201998), number 1384 in Lecture Notes in Computer Science (LNCS), pages 393\u2013408, Lisbon, Portugal, April 1998. Springer-Verlag, Berlin."},{"key":"13_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/3-540-48119-2_13","volume-title":"Proc. of Formal Methods","author":"F. Reffel","year":"1999","unstructured":"F. Reffel and S. Edelkamp. Error Detection with Directed Symbolic Model Checking. In Proc. of Formal Methods, volume 1708 of Lecture Notes in Computer Science, pages 195\u2013211. Springer-Verlag, 1999."},{"key":"13_CR18","unstructured":"T. G. Rokicki. Representing and Modeling Digital Circuits. PhD thesis, Stanford University, 1993."},{"key":"13_CR19","unstructured":"M. Stobbe. Results on scheduling the sidmar steel plant using constraint programming. Internal report, 2000."},{"key":"13_CR20","unstructured":"F. Vaandrager. Analysis of a biphase mark protocol with Uppaal. to appear, 2000."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45319-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T03:10:24Z","timestamp":1556680224000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45319-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418658","9783540453192"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/3-540-45319-9_13","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}