Practical Model Reductions for Verification of Multi-Agent Systems

1 Introduction

Multi-agent systems (MAS) [Wooldridge, 2002; Shoham and Leyton-Brown, 2009] describe interactions of autonomous agents, often assumed to be intelligent and/or rational. With the development of Internet and social networks, the impact of MAS on everyday life is becoming more and more significant. At the same time, their complexity is rapidly increasing. In consequence, formal methods for analysis and verification of MAS are badly needed.

Verification and model reduction. Algorithms and tools for verification have been in constant development for 40 years, with temporal model checking being most popular [Baier and Katoen, 2008; Clarke et al., 2018]. The main obstacle for practical use of those techniques is state-space explosion. Model checking of MAS with respect to their modular representations ranges from PSPACE-complete to undecidable [Schnoebelen, 2003; Jamroga, 2015]. A possible way to mitigate the complexity is by model reductions, such as abstraction refinement [Clarke et al., 2000] and partial-order reduction [Peled, 1993]. Unfortunately, lossless reductions (i.e., ones that produce fully equivalent models) are usually too weak, in the sense that the resulting model is still too large for feasible verification.

Towards practical abstraction. In this work, we revisit the idea of lossy state abstraction [Cousot and Cousot, 1977; Clarke et al., 1994], and in particular may/must abstraction [Godefroid et al., 2001] that potentially removes relevant information about the system, but produces arbitrarily small reduced models. Such verification works best with users who are knowledgeable about the application domain, as its conclusiveness crucially depends on what aspects of the model are being removed. Ideally, the user should be a domain expert, which often implies no in-depth knowledge of verification algorithms. This calls for a technique that is easy to use and understand, preferably supported by a Graphical User Interface (GUI). Moreover, the abstraction should be agent-based in the sense that it operates on modular representations of the MAS, and does not require to generate the full explicitstate model before the reduction. The theoretical backbone of our abstraction scheme is presented in [Jamroga and Kim, 2022]. Here, we report on the implementation, and show its usefulness through case studies.

Contribution. We propose a tool for reduction of MAS models by removing an arbitrary subset of variables from the model specification. After the user selects the variables to be removed, the tool can produce two newmodel specifications: one guaranteed to overapproximate, and one to underapproximate the original model. Then, the user can verify properties of the original model by model checking the new specifications with a suitable model checker. Our model specifications are in the form of MAS Graphs [Jamroga and Kim, 2022], a variant of automata networks with asynchronous execution semantics and synchronization on joint action labels [Priese, 1983; Jamroga et al., 2020]. As the model checker of choice, we use UPPAAL [Behrmann et al., 2004], one of the few temporal model checkers with GUI.

Our tool provides a simple command-line interface, where the user selects the input file with a model specification prepared in UPPAAL, the variables to be abstracted away, and the abstraction parameters. It outputs a file with the over(resp. under-)approximating model specification, that can be opened in UPPAAL for scrutiny and verification. The source code and examples are available at https://tinyurl.com/ ijcai-demo. Importantly, the abstraction uses modular representations for input and output; in fact, it does not involve the generation of the global state space at all. To our best knowledge, this is the first tool for practical user-defined model reductions in model checking of MAS.

Related work. The existing implementations of state abstraction for temporal model checking concern mostly automated abstraction. In particular, CEGAR [Clarke et al., 2000; Clarke et al., 2003] has been implemented for NuSMV [Cimatti et al., 2002], and 3-valued abstraction [Godefroid et al., 2001; Godefroid, 2014] was implemented in Yasm [Gurfinkel et al., 2006] and YOGI [Godefroid et al., 2010]. In each case, abstraction involves the generation of the global state space, which is the main bottleneck when verifying MAS. Other, user-defined abstraction schemes have been defined only theoretically [Shoham and Grumberg, 2004; Ball and Kupferman, 2006; Dams and Grumberg, 2018], and also require to generate all global states and/or transitions. The approaches in [Cohen et al., 2009; Belardinelli et al., 2019] come closest to our work, as they use modular representations of the state space. However, they both need a global representation of the transition space, and no implementation is reported.

2 Formal Background

MAS graphs and templates. To specify the system to be verified, we use MAS graphs, based on standard models of concurrency, and compatible with UPPAAL model specifications. A MAS graph is a multiset of agent graphs, possibly sharing a set of global variables. Each agent graph includes finitely many locations and private variables that, together, define its local state space. Moreover, edges between locations determine the local transition relation. Each edge can be labelled with a randomized selection command, boolean precondition, synchronisation command, and/or a postcondition updating the values of some variables. A synchronizing edge can only be taken with a complementary one in another agent. An example agent graph is shown in Figure 1.

A MAS template treats each agent graph as a template, and specifies the number of its instances that occur in the verified system (each differing only by the value of variable id).

Models. Every MAS graph G can be transformed to its combined MAS graph: technically, a single agent graph comb(G) given by the asynchronous product of the agent graphs in G. Each location in comb(G) is a tuple of agents' locations in G. Moreover, the set of variables in comb(G) is the union of all variables occurring in G. A global model is obtained from comb(G) by unfolding it to the labelled transition system where states are defined by combined locations and valuations of all the variables. Such models are usually huge, and create an important bottleneck in model checking MAS.

Formal verification and model reduction. Our tool addresses model checking of temporal properties expressed in the well known branching-time logic CTL⋆ [Emerson, 1990]. To mitigate the impact of state-space explosion, we use state abstraction, i.e., a method that reduces the state space by clustering similar concrete states into a single abstract state. In order for the scheme to be practical, it must be easy to use, and avoid the generation of the concrete global model. We summarize the details of our abstraction scheme in the next section.

3 Abstraction by Removal of Variables

Our tool employs the abstraction scheme of [Jamroga and Kim, 2022], and produces specifications of two abstract models: a may-abstraction (that overapproximates the concrete states and transitions) and a must-abstraction (that underapproximates them). Consequently, if a universal CTL⋆ formula is true in the may-abstraction, then it must be true in the concrete model, and if it is false in the must-abstraction, then it must be false in the concrete model.

Variable removal. In the simplest variant, the abstraction concerns a complete removal of some variables V ⊆ Var from the model specification. For example, one might remove variables mem vt, mem sg from the agent graph in Figure 1, i.e., the voter's memory of the cast vote and the voting declaration status. Selection of the right variables to remove requires a good understanding of the application domain; we assume that it is provided by the user. Roughly speaking, the abstraction procedure takes the combined MAS graph comb(G), computes an approximation of the reachable values for every v ∈ V , and processes the edges of comb(G) by substituting the occurrences of v at location ℓ with the values u ∈ appr(v, ℓ). If appr(v, ℓ) overapproximates (resp. underapproximates) the actual reachable values of v at ℓ, then the resulting model is a may (resp. must)-abstraction of G.

Variable merge and scoping. More generally, a subset of variables can be merged into a fresh variable by means of a user-defined mapping function. For example, mem sg and mem vt can be merged into a boolean variable valid given by (mem sg*mem vt>0), indicating the validity of the vote.

Additionally the user can specify the scope of abstraction, i.e., a subset of locations where the abstraction is applied.

Abstraction on MAS templates. In some cases, approximation of variable domains on the combined MAS graph is computationally infeasible. An alternative is to compute it directly on the MAS template by the right approximation of the synchronization edges. On the down side, this sometimes results in largely suboptimal abstract models, i.e., ones more likely to produce inconclusive verification results.

4 Architecture

The main components of the tool are: (1) local domain approximation and (2) generation of abstract model specifications. Additionally, the tool allows to perform simple pre-processing and code analysis, and to store parameters in a configuration file. Each component can be called from command line, possibly followed by a list of arguments:

• configure: sets the parameters in the configuration file;
• unfold: produces the combined MAS graph;
• approx: computes an approximation of the local domain;

• abstract: generates an abstract model specification based on the provided approximation of local domain;
• info: lists the variables, locations, and edges in the model.

Local domain approximation. Takes a subset of variables V , a target template ('ext' for the combined MAS graph) and an abstraction type t ∈ {upper, lower}, and computes a tapproximation of the local domain over V . The result is saved to a JSON file, where location identifiers are mapped to an array of evaluation vectors.

Abstract model generation. Takes the mapping function with an upper-approximation (resp. lower-approximation) of the local domain, and computes the corresponding may-abstraction (resp. must-abstraction). The mapping function specifies the target agent name or template name, the scope of abstraction, variables to be removed, and possibly a merge variable. We assume that the input provided by the user is correct; some debugging might be added in the future.

5 Experimental Results

We have evaluated the tool by means of experiments on two benchmarks: a simple postal voting scenario and gossip learning for social AI. The model specifications are available for download with the tool. The experiments have been performed in combination with UPPAAL v4.1.24 (32-bit) on a machine with Intel i7-8665U 2.11 GHz CPU, running Ubuntu 22.04. We report the results for may-abstractions, typically more useful for universal branching-time properties.

Postal voting. We use a scalable family of MAS graphs proposed in [Kim et al., 2022] to model a simplified postal voting system. The system consists of NV Voters, voting for NC candidates, and a single Election Authority, and proceeds in four subsequent phases: collection of voting declarations, preparation and distribution of election packages, ballot casting, and tallying. The verification concerns a variant of resistance to ballot stuffing, expressed by formula φbstuff :

A[](b recv<=ep sent && ep sent<=NV) where b recv and ep sent are variables storing the number of received ballots and sent election packages, respectively. For the experiments, we try the following abstractions:

• A1: removes variables mem vt and mem sg from the Voter template, i.e., the voter's memory of the cast vote and the voting declaration status;
• A2: removes variables mem dec at Voter's locations {has, voted} and variable dec recv at Authority's location {coll vts}, i.e., the information about how the election package has been delivered;
• A3: the combination of A1 and A2.

The results in Table 1 present the numbers of states in the global model generated during the verification, as well as the verification running times (in seconds), including the generation of abstract model specifications where applicable. Formula φbstuff is satisfied in all the reported instances; all three abstractions have been conclusive on it.

Social AI. The second series of experiments uses the specifications of gossip learning for social AI [Heaven, 2013; Heged¨us et al., 2021], proposed in [Kurpiewski et al., 2023]. The system consists of a ring network of AI agents, acting in three phases: data gathering, learning, and sharing of knowledge. The goal of the agents is to collectively reach knowledge of quality mqual ≥ 2. The system includes also an attacker who can impersonate any agent and fake its quality level. The model specification given as asynchronous MAS [Jamroga et al., 2020] and coded in the input language of the STV model checker [Kurpiewski et al., 2021] was manually translated into the input language of UPPAAL. Afterwards, we hardcoded the attacker's strategy to always share the lowest quality model, and verified formula φcompr :

φcompr says that, on all execution paths, at least one AI agent is compromised. The model checking performance is shown in Table 2. We have been able to conduct verification for concrete models with up to 5 agents (4 honest AI and 1 attacker), and up to 7 agents after applying a may-abstraction that discards all variables except for mqual in the AI template.

6 Conclusions

We propose a tool for practical model reductions in multi-agent systems. The tool addresses state-space explosion by removal of selected variables from the model while preserving the truth of ACTL formulas. The experiments show significant gains in terms of verification time as well as memory, with minimal time used by the abstraction procedure.

In the future, we plan to extend our tool to abstractions preserving temporal-epistemic and strategic properties in combination with the MCMAS and STV model checkers [Lomuscio et al., 2017; Kurpiewski et al., 2021].

Acknowledgments

The work was supported by NCBR Poland and FNR Luxembourg under the PolLux/FNR-CORE projects STV (POLLUX-VII/1/2019) and SpaceVote (POLLUXXI/14/SpaceVote/2023), as well as the CHIST-ERA grant CHIST-ERA-19-XAI-010 by NCN Poland (2020/02/Y/ST6/00064).