智能工厂的自动验证与合成

Smart factories, a key ingredient of “Made in China 2025” scheme, aim to use information and communications technologies to digitize the manufacturing processes and reap huge benefits in the form of improved quality, lower costs, and increased efficiency. However, its success heavily relies on the technical developments of autonomous and intelligent systems with multiple agents. This project aims to establish a theoretical foundation on the automated verification and synthesis of smart factories. Based on our prior work of reasoning about knowledge and strategies in multiagent systems, we will study several important issues of smart factories, including reconfigurable manufacturing systems, autonomous decision making of the intelligent components, dynamic joining of new factories or components, and the integration of human and machine intelligence, etc. The main technical challenges include their formal definitions, which need to be aligned with the real industrial applications, and their related computational complexities, which are expected to be completely different with those in automated verification and synthesis of multiagent systems. This foundational work will benefit a future development of software package for the direct development and deployment of various smart factories. The developed techniques can ensure the rigorous correctness of smart factories, and because of its automated nature, can greatly reduce the development cost and time. The project will contribute significantly to the scientific challenge of developing reliable systems, and due to the importance of smart factories and the “Made in China 2025” scheme to the national economy, will greatly benefit the society, the country, and the people.

智能工厂是中国制造2025的核心问题，探索使用计算机技术将工业制造过程数字化以提升产品质量，降低产品成本，并提高生产效率。本项目着眼于建立智能工厂自动验证与合成的理论基础，将研究智能工厂发展的几个重要课题，包括工厂生产的快速重新配置，部件的自主决策，新部件的动态加入，以及人类智能与机器智能的有效整合等。技术上，将基于本团队前期在多智能体系统知识和策略推理方面的大量成果，发展自动化的方法以验证与合成智能工厂。项目的主要的挑战包括对这些智能工厂问题的全新定义，以及对各种问题的计算复杂性的研究。这些基本理论问题的成功解决将对我们原型软件的开发有重要的帮助。技术可被用于严格地保证所开发的智能工厂的正确性，并因技术本身的完全自动化，可以降低开发和维护的成本。将对计算机科学的重要挑战—开发可靠的系统—有很大的贡献，而且因为智能工厂对国民经济发展的重要性，所以也将对国家和人民的利益做出贡献。

多智能体系统 MAS (Multi-Agent Systems)是人工智能的一个重要分支, 本项目以基于逻辑的多智能体系统的自动验证与合成技术为主，辅以认知科学(cognitive sciences)对人行为的分析，发展面向智能工厂的理论基础和计算基础。项目组在智能工厂的逻辑建模、自动验证技术、策略合成方法和底层布尔函数的数据结构优化计算方面取得了一系列突出成果, 发表国际顶尖论文10篇， 其中包括CCF A类会议论文4篇 (AAAI 2篇 , IJCAI 2篇)，CCF B类杂志论文1篇(TCS)和CCF B类会议论文5篇(AAMAS 1篇，ICCAD 2篇，KR 1篇， ETAPS 1篇)，培养了6名研究生。本项目的研究成果将可以为智能工厂各生产要素的交互、合作与协同提供理论工具和计算工具。