Artifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycles, accounting respectively for the relational structure of the artifacts' states and their possible evolutions over time. In this paper we put forward artifact-centric multi-agent systems, a novel formalisation of artifact systems in the context of multi-agent systems operating on them. Differently from the usual process-based models of services, the semantics we give explicitly accounts for the data structures on which artifact systems are defined. We study the model checking problem for artifact-centric multi-agent systems against specifications written in a quantified version of temporal-epistemic logic expressing the knowledge of the agents in the exchange. We begin by noting that the problem is undecidable in general. We then identify two noteworthy restrictions, one syntactical and one semantical, that enable us to find bisimilar finite abstractions and therefore reduce the model checking problem to the instance on finite models. Under these assumptions we show that the model checking problem for these systems is EXPSPACE-complete. We then introduce artifact-centric programs, compact and declarative representations of the programs governing both the artifact system and the agents. We show that, while these in principle generate infinite-state systems, under natural conditions their verification problem can be solved on finite abstractions that can be effectively computed from the programs. Finally we exemplify the theoretical results of the paper through a mainstream procurement scenario from the artifact systems literature.
IFPV: An Integrated Multi-Agent Framework for Generative Operational Planning and High-Fidelity Plan Verification
School of Computer and Artificial Intelligence, Zhengzhou University（郑州大学计算机与人工智能学院）；Engineering Research Center of Intelligent Swarm Systems, Ministry of Education（教育部智能群体系统工程研究中心）；National Supercomputing Center in Zhengzhou（郑州国家超算中心）；Henan Research Center for Large Model Technology（河南省大模型技术与新质软件工程研究中心）
Towards Assume-Guarantee Verification of Abilities in Stochastic Multi-Agent Systems
Institute of Computer Science, Polish Academy of Sciences（波兰科学院计算机科学研究所）；Faculty of Mathematics and Computer Science, Nicolaus Copernicus University（尼古拉·哥白尼大学数学与计算机科学学院）
UCAgent: An End-to-End Agent for Block-Level Functional Verification
State Key Lab of Processors, Institute of Computing Technology, CAS（中国科学院计算技术研究所处理器国家重点实验室）；University of Chinese Academy of Sciences（中国科学院大学）；Beijing Institute of Open Source Chip（北京开源芯片研究院）
