Abstract
We introduce parameterised data-aware multiagent systems, a formalism to reason about the
temporal properties of arbitrarily large collections
of homogeneous agents, each operating on an in-
finite data domain. We show that their parameterised verification problem is semi-decidable for
classes of interest. This is demonstrated by separately addressing the unboundedness of the number of agents and the data domain. In doing so we
reduce the parameterised model checking problem
for these systems to that of parameterised verification for interleaved interpreted systems. We illustrate the expressivity of the formal model by modelling English auctions with an unbounded number
of bidders on unbounded data