King's College London

Research portal

A case study of planning for smart factories: Model checking and Monte Carlo search for the rescue

Research output: Contribution to journalArticle

Stefan Edelkamp, Christoph Greulich

Original languageEnglish
Pages (from-to)515-528
Number of pages14
JournalInternational Journal on Software Tools for Technology Transfer
Issue number5
Early online date7 Aug 2018
Publication statusPublished - 1 Oct 2018

King's Authors


In this work, we propose the application of the SPIN software model checker to a multiagent system that controls the industrial production of goods. The flow of material is buffered on a production line with assembling stations. As the flow of material is asynchronous at each station, queuing is required as long as buffers provide waiting room. Besides validating the design of the system, the core objective of this work is to find concurrent plans that optimize the throughput of the system. In the mapping of the production system to the model checker, we model the production line as a set of communicating processes, with the movement of items modeled as channels. Experiments show that the model checker is able to analyze the system, subject to the partial ordering of the product parts. It derives valid and optimized plans with several thousands of steps using constraint branching in branch-and-bound search. We compare the results with a randomized exploration based on recent advances in Monte Carlo search.

View graph of relations

© 2018 King's College London | Strand | London WC2R 2LS | England | United Kingdom | Tel +44 (0)20 7836 5454