{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,28]],"date-time":"2026-03-28T19:24:56Z","timestamp":1774725896831,"version":"3.50.1"},"reference-count":53,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2018,8,7]],"date-time":"2018-08-07T00:00:00Z","timestamp":1533600000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100009360","name":"King\u2019s College London","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100009360","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,10]]},"DOI":"10.1007\/s10009-018-0498-1","type":"journal-article","created":{"date-parts":[[2018,8,7]],"date-time":"2018-08-07T09:36:04Z","timestamp":1533634564000},"page":"515-528","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A case study of planning for smart factories"],"prefix":"10.1007","volume":"20","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":[[2018,8,7]]},"reference":[{"key":"498_CR1","unstructured":"Abdedda\u00efm, Y., Maler, O.: Job-shop scheduling using timed automata. In: Proceedings of the 13th International Conference on Computer Aided Verification, CAV 2001, Paris, France, July 18\u201322, 2001, pp. 478\u2013492 (2001)"},{"issue":"1","key":"498_CR2","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","volume":"11","author":"A Armando","year":"2009","unstructured":"Armando, A., Mantovani, J., Platania, L.: Bounded model checking of software using SMT solvers instead of SAT solvers. STTT 11(1), 69\u201383 (2009)","journal-title":"STTT"},{"issue":"1","key":"498_CR3","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BF01149329","volume":"1","author":"UN Bhat","year":"1986","unstructured":"Bhat, U.N.: Finite capacity assembly-like queues. Queueing Syst. 1(1), 85\u2013101 (1986)","journal-title":"Queueing Syst."},{"key":"498_CR4","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Zhu, Y.: Symbolic model checking without BDDs. In: Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems, TACAS \u201999, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201999, Amsterdam, The Netherlands, March 22\u201328, 1999, pp. 193\u2013207 (1999)"},{"key":"498_CR5","unstructured":"Bosnacki, D., Dams, D.: Integrating real time into SPIN: A prototype implementation. In: Formal Description Techniques and Protocol Specification, Testing and Verification, FORTE XI\/PSTV XVIII\u201998, IFIP TC6 WG6.1 Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols (FORTE XI) and Protocol Specification, Testing and Verification (PSTV XVIII), 3\u20136 November, 1998, Paris, France, pp. 423\u2013438 (1998)"},{"issue":"1","key":"498_CR6","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/s10009-002-0079-0","volume":"4","author":"E Brinksma","year":"2002","unstructured":"Brinksma, E., Mader, A., Fehnker, A.: Verification and optimization of a PLC control schedule. STTT 4(1), 21\u201333 (2002)","journal-title":"STTT"},{"issue":"7","key":"498_CR7","doi-asserted-by":"publisher","first-page":"697","DOI":"10.1080\/08839510050119253","volume":"14","author":"H B\u00fcrckert","year":"2000","unstructured":"B\u00fcrckert, H., Fischer, K., Vierke, G.: Holonic transport scheduling with teletruck. Appl. Artif. Intell. 14(7), 697\u2013725 (2000)","journal-title":"Appl. Artif. Intell."},{"key":"498_CR8","unstructured":"Burman, M.H.: New results in flow line analysis. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, MA, USA (1995)"},{"key":"498_CR9","doi-asserted-by":"crossref","unstructured":"Cazenave, T.: Nested Monte-Carlo search. In: IJCAI 2009, Proceedings of the 21st International Joint Conference on Artificial Intelligence, Pasadena, California, USA, July 11\u201317, 2009, pp. 456\u2013461 (2009)","DOI":"10.1109\/IPDPS.2009.5161122"},{"key":"498_CR10","unstructured":"Cimatti, A., Giunchiglia, F., Giunchiglia, E., Traverso, P.: Planning via model checking: A decision procedure for AR. In: Recent Advances in AI Planning, 4th European Conference on Planning, ECP\u201997, Toulouse, France, September 24\u201326, 1997, Proceedings, pp. 130\u2013142 (1997)"},{"key":"498_CR11","unstructured":"Cimatti, A., Roveri, M., Traverso, P.: Automatic OBDD-based generation of universal plans in non-deterministic domains. In: Proceedings of the Fifteenth National Conference on Artificial Intelligence and Tenth Innovative Applications of Artificial Intelligence Conference, AAAI 98, IAAI 98, July 26\u201330, 1998, Madison, Wisconsin, USA, pp. 875\u2013881 (1998)"},{"key":"498_CR12","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50026-6","volume-title":"Model Checking","author":"EM Clarke","year":"2001","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2001)"},{"key":"498_CR13","doi-asserted-by":"crossref","unstructured":"Dorer, K., Calisti, M.: An adaptive solution to dynamic transport optimization. In: 4th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2005), July 25\u201329, 2005, Utrecht, The Netherlands - Special Track for Industrial Applications, pp. 45\u201351 (2005)","DOI":"10.1145\/1082473.1082803"},{"key":"498_CR14","unstructured":"Edelkamp, S., Cazenave, T.: Improved diversity in nested rollout policy adaptation. In: KI 2016: Advances in Artificial Intelligence - 39th Annual German Conference on AI, Klagenfurt, Austria, September 26\u201330, 2016, Proceedings, pp. 43\u201355 (2016)"},{"key":"498_CR15","unstructured":"Edelkamp, S., Greulich, C.: Branch-and-bound optimization of a multiagent system for flow production using model checking. In: Proceedings of the 8th International Conference on Agents and Artificial Intelligence (ICAART 2016), Volume 1, Rome, Italy, February 24\u201326, 2016, pp. 27\u201337 (2016)"},{"issue":"2\u20133","key":"498_CR16","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-002-0104-3","volume":"5","author":"S Edelkamp","year":"2004","unstructured":"Edelkamp, S., Leue, S., Lluch-Lafuente, A.: Directed explicit-state model checking in the validation of communication protocols. STTT 5(2\u20133), 247\u2013267 (2004)","journal-title":"STTT"},{"key":"498_CR17","unstructured":"Edelkamp, S., Reffel, F.: OBDDs in heuristic search. In: KI-98: Advances in Artificial Intelligence, 22nd Annual German Conference on Artificial Intelligence, Bremen, Germany, September 15\u201317, 1998, Proceedings, pp. 81\u201392 (1998)"},{"key":"498_CR18","doi-asserted-by":"crossref","unstructured":"Edelkamp, S., Sulewski, D.: Flash-efficient LTL model checking with minimal counterexamples. In: Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM 2008, Cape Town, South Africa, 10\u201314 November 2008, pp. 73\u201382 (2008)","DOI":"10.1109\/SEFM.2008.34"},{"issue":"1","key":"498_CR19","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/088395196118669","volume":"10","author":"K Fischer","year":"1996","unstructured":"Fischer, K., M\u00fcller, J.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":"498_CR20","unstructured":"Fox, M., Long, D.: The detection and exploitation of symmetry in planning problems. In: Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence, IJCAI 99, Stockholm, Sweden, July 31 - August 6, 1999. 2 Volumes, pp. 956\u2013961 (1999)"},{"key":"498_CR21","unstructured":"Ganji, F., Kluge, E.M., Scholz-Reiter, B.: Bringing agents into application: Intelligent products in autonomous logistics. In: Artificial intelligence and Logistics (AiLog)\u2014Workshop at ECAI 2010, pp. 37\u201342 (2010)"},{"key":"498_CR22","doi-asserted-by":"crossref","unstructured":"Gerth, R., Peled, D.A., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995, pp. 3\u201318 (1995)","DOI":"10.1007\/978-0-387-34892-6_1"},{"key":"498_CR23","volume-title":"Automated Planning\u2014Theory and Practice","author":"M Ghallab","year":"2004","unstructured":"Ghallab, M., Nau, D.S., Traverso, P.: Automated Planning\u2014Theory and Practice. Elsevier, Amsterdam (2004)"},{"key":"498_CR24","unstructured":"Giunchiglia, F., Traverso, P.: Planning as model checking. In: Recent Advances in AI Planning, 5th European Conference on Planning, ECP\u201999, Durham, UK, September 8-10, 1999, Proceedings, pp. 1\u201320 (1999)"},{"key":"498_CR25","doi-asserted-by":"crossref","unstructured":"Godefroid, P.: Using partial orders to improve automatic verification methods. In: Computer Aided Verification, 2nd International Workshop, CAV\u201990, New Brunswick, NJ, USA, June 18\u201321, 1990, Proceedings, pp. 176\u2013185 (1990)","DOI":"10.1007\/BFb0023731"},{"key":"498_CR26","unstructured":"Greulich, C., Edelkamp, S., Eicke, N.: Cyber-physical multiagent-simulation in production logistics. In: Multiagent System Technologies\u201413th German Conference, MATES 2015, Cottbus, Germany, September 28\u201330, 2015, Revised Selected Papers, pp. 119\u2013136 (2015)"},{"key":"498_CR27","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. Probab. 10, 354\u2013367 (1973)","journal-title":"J. Appl. Probab."},{"issue":"2","key":"498_CR28","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\u2014application to animal waste management. Comput. Electron. Agric. 63(2), 183\u2013192 (2008)","journal-title":"Comput. Electron. Agric."},{"key":"498_CR29","unstructured":"Himoff, J., Rzevski, G., Skobelev, P.: Magenta technology multi-agent logistics i-scheduler for road transportation. In: 5th International Joint Conference on Autonomous Agents and Multiagent Systems (AAMAS 2006), Hakodate, Japan, May 8\u201312, 2006, pp. 1514\u20131521 (2006)"},{"key":"498_CR30","unstructured":"Hoffmann, J., Kissmann, P., Torralba, \u00c1.: \"distance\"? who cares? tailoring merge-and-shrink heuristics to detect unsolvability. In: ECAI 2014\u201421st European Conference on Artificial Intelligence, 18\u201322 August 2014, Prague, Czech Republic - Including Prestigious Applications of Intelligent Systems (PAIS 2014), pp. 441\u2013446 (2014)"},{"key":"498_CR31","volume-title":"The SPIN Model Checker\u2014Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The SPIN Model Checker\u2014Primer and Reference Manual. Addison-Wesley, Reading (2004)"},{"issue":"2","key":"498_CR32","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/BF01158549","volume":"4","author":"WJ Hopp","year":"1989","unstructured":"Hopp, W.J., Simon, J.T.: Bounds and heuristics for assembly-like queues. Queueing Syst. 4(2), 137\u2013155 (1989)","journal-title":"Queueing Syst."},{"key":"498_CR33","unstructured":"Jensen, R.M., Veloso, M.M., Bowling, M.H.: OBDD-based optimistic and strong cyclic adversarial planning. In: European Symposium on Planning (2001)"},{"key":"498_CR34","unstructured":"Kocsis, L., Szepesv\u00e1ri, C.: Bandit based Monte-Carlo planning. In: Machine Learning: ECML 2006, 17th European Conference on Machine Learning, Berlin, Germany, September 18-22, 2006, Proceedings, pp. 282\u2013293 (2006)"},{"key":"498_CR35","unstructured":"Kupferschmid, S., Hoffmann, J., Dierks, H., Behrmann, G.: Adapting an AI planning heuristic for directed model checking. In: Model Checking Software, 13th International SPIN Workshop, Vienna, Austria, March 30\u2013April 1, 2006, Proceedings, pp. 35\u201352 (2006)"},{"issue":"1","key":"498_CR36","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/BF01149328","volume":"1","author":"EH Lipper","year":"1986","unstructured":"Lipper, E.H., Sengupta, B.: Assembly-like queues with finite capacity: bounds, asymptotics and approximations. Queueing Syst. 1(1), 67\u201383 (1986)","journal-title":"Queueing Syst."},{"key":"498_CR37","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: Proceedings of the 7th International Conference on Hardware\/Software Codesign and System Synthesis, CODES+ISSS 2009, Grenoble, France, October 11\u201316, 2009, pp. 61\u201370 (2009)"},{"key":"498_CR38","unstructured":"Lluch-Lafuente, A.: Symmetry reduction and heuristic search for error detection in model checking. In: Model Checking and Artificial Intelligence (MoChArt), pp. 77\u201386 (2003)"},{"issue":"8","key":"498_CR39","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. OR 35(8), 2520\u20132536 (2008)","journal-title":"Comput. OR"},{"key":"498_CR40","unstructured":"Morales-Kluge, E., Ganji, F., Scholz-Reiter, B.: Intelligent products\u2014towards autonomous logistic processes\u2014a work in progress paper. In: Intern. PLM Conf. (2010)"},{"key":"498_CR41","unstructured":"Nissim, R., Brafman, R.I.: Cost-optimal planning by self-interested agents. In: Proceedings of the Twenty-Seventh AAAI Conference on Artificial Intelligence, July 14\u201318, 2013, Bellevue, Washington, USA (2013)"},{"issue":"2","key":"498_CR42","doi-asserted-by":"publisher","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. J. Betriebswirtschaft 58(2), 81\u2013117 (2008)","journal-title":"J. Betriebswirtschaft"},{"issue":"4","key":"498_CR43","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":"498_CR44","unstructured":"Rosin, C.D.: Nested rollout policy adaptation for Monte Carlo tree search. In: IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16\u201322, 2011, pp. 649\u2013654 (2011)"},{"key":"498_CR45","unstructured":"Ruys, T.C.: Optimal scheduling using branch and bound with SPIN 4.0. In: Model Checking Software, 10th International SPIN Workshop. Portland, OR, USA, May 9\u201310, 2003, Proceedings, pp. 1\u201317 (2003)"},{"key":"498_CR46","unstructured":"Ruys, T.C., Brinksma, E.: Experience with literate programming in the modelling and validation of systems. In: Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS\u201998, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201998, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, pp. 393\u2013408 (1998)"},{"key":"498_CR47","unstructured":"Saffidine, A.: Solving Games and All That. PhD thesis, University Paris\u2013Dauphine (2014)"},{"issue":"7587","key":"498_CR48","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver, D., Huang, A., Maddison, C.J., Guez, A., Sifre, L., van den Driessche, G., Schrittwieser, J., Antonoglou, I., Panneershelvam, V., Lanctot, M., Dieleman, S., Grewe, D., Nham, J., Kalchbrenner, N., Sutskever, I., Lillicrap, T.P., Leach, M., Kavukcuoglu, K., Graepel, T., Hassabis, D.: Mastering the game of Go with deep neural networks and tree search. Nature 529(7587), 484\u2013489 (2016)","journal-title":"Nature"},{"key":"498_CR49","unstructured":"Silver, D., Hubert, T., Schrittwieser, J., Antonoglou, I., Lai, M., Guez, A., Lanctot, M., Sifre, L., Kumaran, D., Graepel, T., Lillicrap, T.P., Simonyan, K., Hassabis, D.: Mastering Chess and Shogi by self-play with a general reinforcement learning algorithm. CoRR arXiv:1712.01815 (2017)"},{"issue":"4","key":"498_CR50","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/BF00709154","volume":"1","author":"A Valmari","year":"1992","unstructured":"Valmari, A.: A stubborn attack on state explosion. Form. Methods Syst. Des. 1(4), 297\u2013322 (1992)","journal-title":"Form. Methods Syst. Des."},{"key":"498_CR51","unstructured":"Wijs, A.: What to do Next? Analysing and Optimising System Behaviour in Time. PhD thesis, Vrije Universiteit Amsterdam (2007)"},{"key":"498_CR52","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5804.001.0001","volume-title":"Reasoning about Rational Agents","author":"MJ Wooldridge","year":"2000","unstructured":"Wooldridge, M.J.: Reasoning about Rational Agents. The MIT Press, Cambridge (2000)"},{"key":"498_CR53","volume-title":"An Introduction to MultiAgent Systems","author":"MJ Wooldridge","year":"2009","unstructured":"Wooldridge, M.J.: An Introduction to MultiAgent Systems, 2nd edn. Wiley, New York (2009)","edition":"2"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-018-0498-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0498-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-018-0498-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T07:06:33Z","timestamp":1751785593000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-018-0498-1"}},"subtitle":["Model checking and Monte Carlo search for the rescue"],"short-title":[],"issued":{"date-parts":[[2018,8,7]]},"references-count":53,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["498"],"URL":"https:\/\/doi.org\/10.1007\/s10009-018-0498-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,8,7]]},"assertion":[{"value":"7 August 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}