{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T01:40:08Z","timestamp":1749951608819,"version":"3.41.0"},"publisher-location":"Cham","reference-count":48,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319533537"},{"type":"electronic","value":"9783319533544"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-53354-4_2","type":"book-chapter","created":{"date-parts":[[2017,2,6]],"date-time":"2017-02-06T08:12:49Z","timestamp":1486368769000},"page":"19-36","source":"Crossref","is-referenced-by-count":0,"title":["Two Model Checking Approaches to Branch-and-Bound Optimization of a Flow Production System"],"prefix":"10.1007","author":[{"given":"Christoph","family":"Greulich","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Edelkamp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,7]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/11691617_9","volume-title":"Model Checking Software","author":"A Armando","year":"2006","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 146\u2013162. Springer, Heidelberg (2006). doi: 10.1007\/11691617_9"},{"key":"2_CR2","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1007\/BF01149329","volume":"1","author":"U Bhat","year":"1986","unstructured":"Bhat, U.: Finite capacity assembly-like queues. Queueing Syst. 1, 85\u2013101 (1986)","journal-title":"Queueing Syst."},{"key":"2_CR3","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). doi: 10.1007\/3-540-49059-0_14"},{"key":"2_CR4","first-page":"423","volume-title":"FORTE\/PSTV","author":"D Bo\u0161na\u010dki","year":"1998","unstructured":"Bo\u0161na\u010dki, D., Dams, D.: Integrating real time into spin: a prototype implementation. In: Budkowski, S., Cavalli, A., Najm, E. (eds.) FORTE\/PSTV, vol. 6, pp. 423\u2013438. Springer, New York (1998)"},{"key":"2_CR5","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-88973-1","volume-title":"Digitale Fabrik: Methoden und Praxisbeispiele","author":"U Bracht","year":"2011","unstructured":"Bracht, U., Geckler, D., Wenzel, S.: Digitale Fabrik: Methoden und Praxisbeispiele. Springer, Heidelberg (2011)"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/10722468_5","volume-title":"SPIN Model Checking and Software Verification","author":"E Brinksma","year":"2000","unstructured":"Brinksma, E., Mader, A.: Verification and optimization of a PLC control schedule. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 73\u201392. Springer, Heidelberg (2000). doi: 10.1007\/10722468_5"},{"issue":"7","key":"2_CR7","doi-asserted-by":"crossref","first-page":"697","DOI":"10.1080\/08839510050119253","volume":"14","author":"HJ B\u00fcrckert","year":"2000","unstructured":"B\u00fcrckert, H.J., Fischer, K., Vierke, G.: Holonic transport scheduling with teletruck. Appl. Artif. Intell. 14(7), 697\u2013725 (2000)","journal-title":"Appl. Artif. Intell."},{"key":"2_CR8","unstructured":"Burman, M.: New results in flow line analysis. Ph.D. thesis, Massachusetts Institute of Technology (1995)"},{"key":"2_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/3-540-63912-8_81","volume-title":"Recent Advances in AI Planning","author":"A Cimatti","year":"1997","unstructured":"Cimatti, A., Giunchiglia, E., Giunchiglia, F., Traverso, P.: Planning via model checking: a decision procedure for AR. In: Steel, S., Alami, R. (eds.) ECP 1997. LNCS, vol. 1348, pp. 130\u2013142. Springer, Heidelberg (1997). doi: 10.1007\/3-540-63912-8_81"},{"key":"2_CR10","unstructured":"Cimatti, A., Roveri, M., Traverso, P.: Automatic OBDD-based generation of universal plans in non-deterministic domains. In: AAAI, pp. 875\u2013881 (1998)"},{"key":"2_CR11","volume-title":"Model Checking","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Dorer, K., Calisti, M.: An adaptive solution to dynamic transport optimization. In: AAMAS, pp. 45\u201351. ACM (2005)","DOI":"10.1145\/1082473.1082803"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45139-0_5","volume-title":"Model Checking Software","author":"S Edelkamp","year":"2001","unstructured":"Edelkamp, S., Lafuente, A.L., Leue, S.: Directed explicit model checking with HSF-SPIN. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 57\u201379. Springer, Heidelberg (2001). doi: 10.1007\/3-540-45139-0_5"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/BFb0095430","volume-title":"KI-98: Advances in Artificial Intelligence","author":"S Edelkamp","year":"1998","unstructured":"Edelkamp, S., Reffel, F.: OBDDs in heuristic search. In: Herzog, O., G\u00fcnter, A. (eds.) KI 1998. LNCS, vol. 1504, pp. 81\u201392. Springer, Heidelberg (1998). doi: 10.1007\/BFb0095430"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Sulewski, D.: Flash-efficient LTL model checking with minimal counterexamples. In: SEFM, pp. 73\u201382 (2008)","DOI":"10.1109\/SEFM.2008.34"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-319-32582-8_4","volume-title":"Model Checking Software","author":"S Edelkamp","year":"2016","unstructured":"Edelkamp, S., Greulich, C.: Using SPIN for the optimized scheduling of discrete event systems in manufacturing. In: Bo\u0161na\u010dki, D., Wijs, A. (eds.) SPIN 2016. LNCS, vol. 9641, pp. 57\u201377. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-32582-8_4"},{"issue":"1","key":"2_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1080\/088395196118669","volume":"10","author":"K Fischer","year":"1996","unstructured":"Fischer, K., M\u00fcller, J.R.P., Pischel, M.: Cooperative transportation scheduling: an application domain for DAI. Appl. Artif. Intell. 10(1), 1\u201334 (1996)","journal-title":"Appl. Artif. Intell."},{"key":"2_CR18","unstructured":"Fox, M., Long, D.: The detection and exploration of symmetry in planning problems. In: IJCAI, pp. 956\u2013961 (1999)"},{"key":"2_CR19","volume-title":"Parallel and Distributed Simulation Systems","author":"R Fujimoto","year":"2000","unstructured":"Fujimoto, R.: Parallel and Distributed Simulation Systems. Wiley, Hoboken (2000)"},{"key":"2_CR20","unstructured":"Ganji, F., Morales Kluge, E., Scholz-Reiter, B.: Bringing agents into application: intelligent products in autonomous logistics. In: Schill, K., Scholz-Reiter, B., Frommberger, L. (eds.) Artificial Intelligence and Logistics (AiLog) - Workshop at ECAI 2010, pp. 37\u201342 (2010)"},{"key":"2_CR21","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D., Vardi, M., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: PSTV, pp. 3\u201318. Chapman & Hall (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/10720246_1","volume-title":"Recent Advances in AI Planning","author":"F Giunchiglia","year":"2000","unstructured":"Giunchiglia, F., Traverso, P.: Planning as model checking. In: Biundo, S., Fox, M. (eds.) ECP 1999. LNCS (LNAI), vol. 1809, pp. 1\u201320. Springer, Heidelberg (2000). doi: 10.1007\/10720246_1"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/BFb0023731","volume-title":"Computer-Aided Verification","author":"P Godefroid","year":"1991","unstructured":"Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176\u2013185. Springer, Heidelberg (1991). doi: 10.1007\/BFb0023731"},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-319-27343-3_7","volume-title":"Multiagent System Technologies","author":"C Greulich","year":"2015","unstructured":"Greulich, C., Edelkamp, S., Eicke, N.: Cyber-physical multiagent-simulation in production logistics. In: M\u00fcller, J.P., Ketter, W., Kaminka, G., Wagner, G., Bulling, N. (eds.) MATES 2015. LNCS (LNAI), vol. 9433, pp. 119\u2013136. Springer, Heidelberg (2015). doi: 10.1007\/978-3-319-27343-3_7"},{"key":"2_CR25","doi-asserted-by":"crossref","first-page":"354","DOI":"10.1017\/S0021900200095358","volume":"10","author":"J Harrison","year":"1973","unstructured":"Harrison, J.: Assembly-like queues. J. Appl. Probab. 10, 354\u2013367 (1973)","journal-title":"J. Appl. Probab."},{"issue":"2","key":"2_CR26","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/j.compag.2008.02.008","volume":"63","author":"A Helias","year":"2008","unstructured":"Helias, A., Guerrin, F., Steyer, J.P.: Using timed automata and model-checking to simulate material flow in agricultural production systems - application to animal waste management. Comput. Electron. Agric. 63(2), 183\u2013192 (2008)","journal-title":"Comput. Electron. Agric."},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Himoff, J., Rzevski, G., Skobelev, P.: Magenta technology multi-agent logistics i-scheduler for road transportation. In: AAMAS, pp. 1514\u20131521. ACM (2006)","DOI":"10.1145\/1160633.1160927"},{"key":"2_CR28","unstructured":"Hoffmann, J., Kissmann, P., Torralba, \u00c1.: \u201cDistance\u201d? Who cares? Tailoring merge-and-shrink heuristics to detect unsolvability. In: ECAI, pp. 441\u2013446 (2014)"},{"key":"2_CR29","volume-title":"The SPIN Model Checker - Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"2_CR30","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1007\/BF01158549","volume":"4","author":"W Hopp","year":"1989","unstructured":"Hopp, W., Simon, J.: Bounds and heuristics for assembly-like queues. Queueing Syst. 4, 137\u2013156 (1989)","journal-title":"Queueing Syst."},{"key":"2_CR31","unstructured":"Jensen, R.M., Veloso, M.M., Bowling, M.H.: OBDD-based optimistic and strong cyclic adversarial planning. In: ECP (2001)"},{"key":"2_CR32","unstructured":"Kautz, H., Selman, B.: Pushing the envelope: planning propositional logic, and stochastic search. In: ECAI, pp. 1194\u20131201 (1996)"},{"key":"2_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11691617_3","volume-title":"Model Checking Software","author":"S Kupferschmid","year":"2006","unstructured":"Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol. 3925, pp. 35\u201352. Springer, Heidelberg (2006). doi: 10.1007\/11691617_3"},{"key":"2_CR34","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1007\/BF01149328","volume":"1","author":"E Lipper","year":"1986","unstructured":"Lipper, E., Sengupta, E.: Assembly-like queues with finite capacity: bounds, asymptotics and approximations. Queueing Syst. 1, 67\u201383 (1986)","journal-title":"Queueing Syst."},{"key":"2_CR35","unstructured":"Lluch-Lafuente, A.: Symmetry reduction and heuristic search for error detection in model checking. In: MOCHART, pp. 77\u201386 (2003)"},{"issue":"8","key":"2_CR36","doi-asserted-by":"crossref","first-page":"2520","DOI":"10.1016\/j.cor.2006.12.016","volume":"35","author":"M Manitz","year":"2008","unstructured":"Manitz, M.: Queueing-model based analysis of assembly lines with finite buffers and general service times. Comput. Oper. Res. 35(8), 2520\u20132536 (2008)","journal-title":"Comput. Oper. Res."},{"key":"2_CR37","unstructured":"Morales Kluge, E., Ganji, F., Scholz-Reiter, B.: Intelligent products - towards autonomous logistic processes - a work in progress paper. In: PLM, Bremen, pp. 348\u2013357 (2010)"},{"key":"2_CR38","volume-title":"Automated Planning: Theory & Practice","author":"D Nau","year":"2004","unstructured":"Nau, D., Ghallab, M., Traverso, P.: Automated Planning: Theory & Practice. Morgan Kaufmann Publishers Inc., San Francisco (2004)"},{"key":"2_CR39","doi-asserted-by":"crossref","unstructured":"Nissim, R., Brafman, R.I.: Cost-optimal planning by self-interested agents. In: AAAI (2013)","DOI":"10.1609\/aaai.v27i1.8640"},{"issue":"2","key":"2_CR40","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/s11301-008-0036-4","volume":"58","author":"SN Parragh","year":"2008","unstructured":"Parragh, S.N., Doerner, K.F., Hartl, R.F.: A survey on pickup and delivery problems Part II: transportation between pickup and delivery locations. J. f\u00fcr Betriebswirtschaft 58(2), 81\u2013117 (2008)","journal-title":"J. f\u00fcr Betriebswirtschaft"},{"issue":"4","key":"2_CR41","first-page":"25","volume":"23","author":"H Rekersbrink","year":"2007","unstructured":"Rekersbrink, H., Ludwig, B., Scholz-Reiter, B.: Entscheidungen selbststeuernder logistischer Objekte. Ind. Manag. 23(4), 25\u201330 (2007)","journal-title":"Ind. Manag."},{"key":"2_CR42","volume-title":"Artificial Intelligence - A Modern Approach","author":"SJ Russell","year":"2010","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence - A Modern Approach, 3rd edn. Pearson Education, Upper Saddle River (2010)","edition":"3"},{"key":"2_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44829-2_1","volume-title":"Model Checking Software","author":"TC Ruys","year":"2003","unstructured":"Ruys, T.C.: Optimal scheduling using branch and bound with SPIN 4.0. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 1\u201317. Springer, Heidelberg (2003). doi: 10.1007\/3-540-44829-2_1"},{"key":"2_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1007\/BFb0054185","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"TC Ruys","year":"1998","unstructured":"Ruys, T.C., Brinksma, E.: Experience with literate programming in the modelling and validation of systems. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 393\u2013408. Springer, Heidelberg (1998). doi: 10.1007\/BFb0054185"},{"key":"2_CR45","unstructured":"Saffidine, A.: Solving games and all that. Ph.D. thesis, University Paris-Dauphine (2014)"},{"key":"2_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/BFb0023729","volume-title":"Computer-Aided Verification","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156\u2013165. Springer, Heidelberg (1991). doi: 10.1007\/BFb0023729"},{"key":"2_CR47","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5804.001.0001","volume-title":"Reasoning About Rational Agents","author":"M Wooldridge","year":"2000","unstructured":"Wooldridge, M.: Reasoning About Rational Agents. The MIT Press, Cambridge (2000)"},{"key":"2_CR48","volume-title":"An Introduction to Multi-agent Systems","author":"M Wooldridge","year":"2002","unstructured":"Wooldridge, M.: An Introduction to Multi-agent Systems. Wiley, Chichester (2002)"}],"container-title":["Lecture Notes in Computer Science","Agents and Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-53354-4_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T01:07:41Z","timestamp":1749949661000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-53354-4_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319533537","9783319533544"],"references-count":48,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-53354-4_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}