JustAct+: A Framework for Auditable Multi-Agent Systems Regulated by Inter-Organisational Policies

TL;DR

JustAct+ is a framework that enables auditable, policy-regulated multi-agent systems, ensuring actions are justified by collected policy information and maintaining key properties like non-refutability of permissions.

Contribution

It introduces a formal framework for policy-based regulation in multi-agent systems, with proofs of key properties and a practical implementation in Rust.

Findings

Proves that permitted actions cannot be refuted later in the system.

Develops a specific policy language and runtime system in Rocq and Rust.

Demonstrates the framework's applicability through a medical data processing case study.

Abstract

In open multi-agent agent systems that cross organisational boundaries, agent actions must be regulated by complex policies. Consider medical data processing systems, which must observe generic laws (e.g., EU data protection regulations) and also specific participants' resource conditions (e.g., Bob consents to sharing his X-Rays with EU hospitals). Presently, we address the implementation of these systems as distributed software. Solutions to key sub-problems are available: existing policy languages capture the necessary normative concepts and formalise the computational representation and reasoning about policies, and existing distributed algorithms and protocols coordinate agents' changing actions and policies. But which policies and protocols are useful in application? With the JustAct framework, we characterise a class of multi-agent systems where actors justify their actions with sufficient policy information collected from dynamic policy statements and agreements. We prove key properties of these systems, e.g., any decision that an action is permitted now cannot be refuted later, regardless of any added statements or updated agreements. We study a particular instance of the framework by specifying (in Rocq) and implementing (in Rust) a particular policy language and runtime system for mediating agent communications. We demonstrate and assess JustAct via a case study of this implementation: we reproduce the usage scenarios of Brane, an existing policy-regulated, inter-domain, medical data processing system.