{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T03:39:44Z","timestamp":1725853184874},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319325811"},{"type":"electronic","value":"9783319325828"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","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":[[2016]]},"DOI":"10.1007\/978-3-319-32582-8_4","type":"book-chapter","created":{"date-parts":[[2016,4,7]],"date-time":"2016-04-07T10:04:23Z","timestamp":1460023463000},"page":"57-77","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Using SPIN for the Optimized Scheduling of Discrete Event Systems in Manufacturing"],"prefix":"10.1007","author":[{"given":"Stefan","family":"Edelkamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Christoph","family":"Greulich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,8]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/3-540-44585-4_46","volume-title":"Computer Aided Verification","author":"Y Abdedda\u00efm","year":"2001","unstructured":"Abdedda\u00efm, Y., Maler, O.: Job-shop scheduling using timed automata. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 478. Springer, Heidelberg (2001)"},{"key":"4_CR2","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)"},{"key":"4_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5237-6","volume-title":"Multiobjective Scheduling by Genetic Algorithms","author":"TP Bagchi","year":"1999","unstructured":"Bagchi, T.P.: Multiobjective Scheduling by Genetic Algorithms. Springer, USA (1999)"},{"key":"4_CR4","doi-asserted-by":"publisher","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":"4_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 of 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, p. 193. Springer, Heidelberg (1999)"},{"key":"4_CR6","first-page":"423","volume-title":"FORTE\/PSTV","author":"D Bosnacki","year":"1998","unstructured":"Bosnacki, D., Dams, D.: Integrating real time into spin: a prototype implementation. In: Budkowski, S., Cavalli, A., Najm, E. (eds.) FORTE\/PSTV, pp. 423\u2013438. Springer, New York (1998)"},{"key":"4_CR7","first-page":"73","volume":"1885","author":"E Brinksma","year":"2000","unstructured":"Brinksma, E., Mader, A.: Verification and optimization of a PLC control schedule. SPIN 1885, 73\u201392 (2000)","journal-title":"SPIN"},{"key":"4_CR8","unstructured":"Burman, M.: New results in flow line analysis. Ph.D. thesis, Massachusetts Institute of Technology (1995)"},{"key":"4_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. (ed.) ECP 1997. LNCS, vol. 1348, pp. 130\u2013142. Springer, Heidelberg (1997)"},{"key":"4_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":"4_CR11","volume-title":"Model Checking","author":"E Clarke","year":"2000","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Lluch-Lafuente, A., Leue, S.: Directed model-checking in HSF-SPIN. In: SPIN, pp. 57\u201379 (2001)","DOI":"10.1007\/3-540-45139-0_5"},{"key":"4_CR13","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. (ed.) KI 1998. LNCS, vol. 1504, pp. 81\u201392. Springer, Heidelberg (1998)"},{"key":"4_CR14","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":"4_CR15","unstructured":"Fox, M., Long, D.: The detection and exploration of symmetry in planning problems. In: IJCAI, pp. 956\u2013961 (1999)"},{"issue":"2","key":"4_CR16","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1287\/moor.1.2.117","volume":"1","author":"MR Garey","year":"1976","unstructured":"Garey, M.R., Johnson, D.S., Sethi, R.: The complexity of flowshop and jobshop scheduling. Math. Oper. Res. 1(2), 117\u2013129 (1976)","journal-title":"Math. Oper. Res."},{"key":"4_CR17","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 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","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, vol. 1809, pp. 1\u201319. Springer, Heidelberg (2000)"},{"key":"4_CR19","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., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176\u2013185. Springer, Heidelberg (1991)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Greulich, C., Edelkamp, S.: Branch-and-bound optimization of a multiagent system for flow production using model checking. In: ICAART (2016)","DOI":"10.5220\/0005705100270037"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","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., et al. (eds.) MATES 2015. LNCS, vol. 9433, pp. 119\u2013136. Springer, Heidelberg (2015). doi:\n                    10.1007\/978-3-319-27343-3_7"},{"key":"4_CR22","doi-asserted-by":"publisher","first-page":"354","DOI":"10.2307\/3212352","volume":"10","author":"J Harrison","year":"1973","unstructured":"Harrison, J.: Assembly-like queues. J. Appl. Prob. 10, 354\u2013367 (1973)","journal-title":"J. Appl. Prob."},{"issue":"2","key":"4_CR23","doi-asserted-by":"publisher","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. Electr. Agric. 63(2), 183\u2013192 (2008)","journal-title":"Comput. Electr. Agric."},{"key":"4_CR24","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":"4_CR25","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":"4_CR26","doi-asserted-by":"publisher","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":"4_CR27","unstructured":"Jensen, R.M., Veloso, M.M., Bowling, M.H.: OBDD-based optimistic and strong cyclic adversarial planning. In: ECpP (2001)"},{"key":"4_CR28","unstructured":"Kautz, H., Selman, B.: Pushing the envelope: planning propositional logic, and stochastic search. In: ECAI, pp. 1194\u20131201 (1996)"},{"key":"4_CR29","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)"},{"issue":"1","key":"4_CR30","doi-asserted-by":"publisher","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(1), 67\u201383 (1986)","journal-title":"Queueing Syst."},{"key":"4_CR31","doi-asserted-by":"crossref","unstructured":"Liu, W., Gu, Z., Xu, J., Wang, Y., Yuan, M.: An efficient technique for analysis of minimal buffer requirements of synchronous dataflow graphs with model checking. In: CODES+ISSS, pp. 61\u201370 (2009)","DOI":"10.1145\/1629435.1629445"},{"key":"4_CR32","unstructured":"Lluch-Lafuente, A.: Symmetry reduction and heuristic search for error detection in model checking. In: MOCHART, pp. 77\u201386 (2003)"},{"issue":"8","key":"4_CR33","doi-asserted-by":"publisher","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":"4_CR34","unstructured":"Morales Kluge, E., Ganji, F., Scholz-Reiter, B.: Intelligent products - towards autonomous logistic processes - a work in progress paper. In: International PLM Conference (2010)"},{"key":"4_CR35","volume-title":"Automated Planning: Theory and Practice","author":"D Nau","year":"2004","unstructured":"Nau, D., Ghallab, M., Traverso, P.: Automated Planning: Theory and Practice. Morgan Kaufmann Publishers Inc., San Francisco (2004)"},{"key":"4_CR36","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)"},{"key":"4_CR37","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 mode-lling and validation of systems. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, p. 393. Springer, Heidelberg (1998)"},{"issue":"4","key":"4_CR38","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1109\/TSMCC.2006.874022","volume":"36","author":"W Shen","year":"2006","unstructured":"Shen, W., Wang, L., Hao, Q.: Planning, agent-based distributed manufacturing process scheduling: a state-of-the-art survey. IEEE Trans. Syst. Man Cybern., Part\u00a0C (Appl. Rev.) 36(4), 563\u2013577 (2006)","journal-title":"IEEE Trans. Syst. Man Cybern., Part\u00a0C (Appl. Rev.)"},{"key":"4_CR39","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/BFb0023729","volume":"531","author":"A Valmari","year":"1991","unstructured":"Valmari, A.: A stubborn attack on state explosion. Lect. Notes Comput. Sci. 531, 156\u2013165 (1991)","journal-title":"Lect. Notes Comput. Sci."},{"key":"4_CR40","unstructured":"Wijs, A.: What to do next? analysing and optimising system behaviour in time. Ph.D. thesis, Vrije Universiteit Amsterdam (2007)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-32582-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,24]],"date-time":"2020-03-24T01:17:53Z","timestamp":1585012673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-32582-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319325811","9783319325828"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-32582-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"8 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}