Two Model Checking Approaches to Branch-and-Bound Optimization of a Flow Production System

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2017
• 出版时间：2017
• 年：2017
• 卷：10162
• 期：1
• 页码：19-36
• 丛书名：Agents and Artificial Intelligence
• ISBN：978-3-319-53354-4
• 卷排序：10162

文摘

In this paper we introduce a novel application of model checking to find optimal planning solutions for a flow production system. Originally controlled by a multiagent system, the production system consists of autonomous products and asynchronous production stations with limited space for waiting products. In this work, we present two different approaches of application of the Spin model checker to optimize throughput in the given production system. Instead of mapping the multiagent system directly, we model the production line itself as a set of communicating processes. Each communication channel between two processes represents a one-way monorail connection from one station to another. Experiments show that both approaches derive valid and optimized plans with several thousands of steps using constrained branch-and-bound. However, experiments also indicate individual advantages of both approaches.