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

3Citations
Citations of this article
16Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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.

Cite

CITATION STYLE

APA

Edelkamp, S., & Greulich, C. (2018). A case study of planning for smart factories: Model checking and Monte Carlo search for the rescue. International Journal on Software Tools for Technology Transfer, 20(5), 515–528. https://doi.org/10.1007/s10009-018-0498-1

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free