Verification of Relational Multiagent Systems with Data Types (Extended Version)

TL;DR

This paper extends the verification of relational multiagent systems to include data types with dense linear orders, providing a decidability result under certain conditions and a finite-state abstraction approach.

Contribution

It introduces a novel approach to verify RMASs with dense linear orders and facets, expanding previous decidability results under the state-bounded assumption.

Findings

Decidability achieved with dense linear orders and facets.

Finite-state, sound, and complete abstraction constructed.

Undecidability shown with successor relation data types.

Abstract

We study the extension of relational multiagent systems (RMASs), where agents manipulate full-fledged relational databases, with data types and facets equipped with domain-specific, rigid relations (such as total orders). Specifically, we focus on design-time verification of RMASs against rich first-order temporal properties expressed in a variant of first-order mu-calculus with quantification across states. We build on previous decidability results under the "state-bounded" assumption, i.e., in each single state only a bounded number of data objects is stored in the agent databases, while unboundedly many can be encountered over time. We recast this condition, showing decidability in presence of dense, linear orders, and facets defined on top of them. Our approach is based on the construction of a finite-state, sound and complete abstraction of the original system, in which dense linear orders are reformulated as non-rigid relations working on the active domain of the system only. We also show undecidability when including a data type equipped with the successor relation.