Model Checking Auctions as Artifact Systems: Decidability via Finite Abstraction

Abstract. The formal verification of auctions has recently received considerable attention in the AI and logic community. We tackle this problem by adopting methodologies and techniques originally de-veloped for Artifact Systems, a novel paradigm in Service Oriented Computing. Specifically, we introduce a typed version of artifact-centric multi-agent systems (AC-MAS), a multi-agent setting for Ar-tifact Systems, and consider the model checking problem against typed first-order temporal epistemic specifications. Notably, this for-mal framework is expressive enough to capture a relevant class of auctions: parallel English (ascending bid) auctions. We prove decid-ability of the model checking problem for AC-MAS via finite ab-straction. In particular, we put forward a methodology to formally verify interesting properties of auctions.