NatSTV: Towards Verification of Natural Strategic Ability

1 Introduction

Multi-agent systems (MAS) are based on the interaction of multiple autonomous agents, some of them intelligent and/or proactive, often exhibiting purposeful collaborative (or, conversely, adversarial) behavior. Formal methods for analysis and verification are essential to ascertain their functionality and security. Alternating-time temporal logic ATL [Alur et al., 2002; Schobbens, 2004] is a widely recognized framework for reasoning about the strategic abilities of agents, that enables to address the potential outcomes of individual agents and their coalitions. Over the past two decades, substantial effort has been devoted to algorithms for formal verification of strategic logics [Alur et al., 2002; Mogavero et al., 2014; Chen et al., 2013; Busard et al., 2014; Huang and van der Meyden, 2014; Cermak et al., 2014; Cermák et al., 2015; Jamroga et al., 2019a]. Based on those, a number of model checking tools have been developed, including Mocha [Alur et al., 1998], MCMAS [Lomuscio et al., 2017] and VITAMIN [Ferrando and Malvone, 2024]. However, the computational complexity of model checking for strategic abilities, especially under imperfect information, is very challenging [Bulling et al., 2010; Jamroga, 2015].

To address the challenges, our group at the Polish Academy of Sciences has developed a suite of techniques for incomplete and approximate verification of ATL for agents with imperfect information, implemented in our experimental open-source model checker STV (STrategic Verifier) [Kurpiewski et al., 2019; Kurpiewski et al., 2021; Kaminski et al., 2024; Kurpiewski et al., 2024]. Here, we expand the suite with sound but incomplete verification of natural strategic ability, expressed in "Natural ATL," or NatATL [Jamroga et al., 2019b; Jamroga et al., 2019c].

The new tool, called NatSTV, provides a user-friendly environment for analyzing such requirements, featuring a graphical user interface (GUI) and a flexible model specification language. Thanks to that, it has significant pedagogical value, serving as an intuitive introduction to the complex subjects of strategic reasoning and model checking of strategic logics. Previous versions of STV have been utilized in tutorials and graduate courses at top AI conferences and summer schools, including IJCAI 2022, PRIMA 2022, ESSAI 2023, and ECAI 2024. The only other tool to synthesize and verify natural strategies is a very recent extension of VITAMIN [Aruta et al., 2024]. However, it only tackles the case of perfect information strategies, whereas NatSTV verifies MAS with imperfect information (i.e., partial observability).

2 Application Domain

NatSTV addresses the formal verification of strategic abilities in multi-agent systems. ATL formulas like ⟨⟨taxi, passg⟩⟩♢destination ("the autonomous cab and the passenger have a joint strategy to eventually arrive at the destination") and ⟨⟨passg⟩⟩□alive ("the passenger can keep staying alive") can be used to express important functionality, safety, and security requirements in MAS [Jamroga, 2015]. This is, e.g., relevant for specification and verification of e-voting. Properties such as anonymity, coercionresistance, and voter verifiability are crucial for voting procedures, and have a strong strategic component. However, case studies [Jamroga et al., 2018; Jamroga et al., 2020b; Kurpiewski et al., 2022] have demonstrated that practical verification of those properties is infeasible due to the state-, transition- and strategy-space explosion.

Natural strategies were proposed in [Jamroga et al., 2019b; Jamroga et al., 2019c] to capture the abilities of agents with limited computational resources, such as humans, drones, sensor networks etc. In particular, natural strategic abilities provide a more suitable semantics for reasoning about what human voters can plausibly achieve [Jamroga et al., 2021a]. Extensions of NatATL have been used to analyze the abilities of participants in keyword auctions and probabilistic access control [Belardinelli et al., 2022; Berthon et al., 2024].

NatSTV is our first step towards practical verification of such abilities. Given a modular specification of a MAS and a formula ⟨⟨A⟩⟩γ, it attempts to synthesize and simplify a natural strategy for A to enforce the temporal property γ. Then, it reports the size k of the smallest natural strategy that has been found. Thus, for all complexity constraints of k′ ≥ k, we get that the NatATL formula ⟨⟨A⟩⟩≤k′ γ holds. In this sense, NatSTV provides sound but not complete model checking for NatATL with imperfect information.

3 Formal Background

Model checking takes a specification of the system model M and a logical formula φ, and asks if φ is satisfied by M.

Modules and models. The primary input consists of a collection of asynchronous modules [Lomuscio et al., 2013; Jamroga et al., 2020a], where each local state consists of a location label, possibly with a valuation of state variables. Local transitions in an agent's module are determined by the current location, the choice of the agent, and possibly the valuation of input variables. They can be either private or shared between several agents. In the latter case, the transition can be executed only if all the involved agents synchronously participate in it. An example specification of an agent module in the input language of NatSTV is shown in Figure 1.

The global model of the MAS is given by the asynchronous product of its modules. In particular, global states are tuples of local states, one per agent, reachable from the initial configuration, cf. [Jamroga et al., 2021b; Kurpiewski et al., 2022] for the details.

General strategies. A strategy is a conditional plan that prescribes the agents' actions for every possible situation [Alur et al., 2002; Schobbens, 2004]. We focus on imperfect information memoryless strategies, which are functions mapping the agent's local states to its available choices. The outcome of a strategy from state q consists of all infinite paths starting from q that are consistent with the strategy.

Natural strategies. Let B(Prop) denote the set of Boolean formulas over some atomic propositions P rop. Natural memoryless strategies for agent a are represented by ordered lists of guarded actions. That is, sa consists of pairs ϕi ⇝ αi where ϕi ∈ B(Prop) and αi is a choice available to a in states where ϕi holds. To enforce that only uniform (i.e., executable) strategies are used, we impose that only the local atomic propositions of module a can be used within sa. A collective strategy sA is simply a tuple of individual strategies, one per a ∈ A.

Complexity of strategies. The complexity of a natural strategy sA is defined as compl (sA) = ∑(ϕ,α)∈sA |ϕ|, where |ϕ| represents the number of symbols in the guard ϕ, excluding parentheses. Thus, compl (sA) measures the total length of the guards in sA.

Logic. Given a model M and a state q in M, the ATL formula ⟨⟨A⟩⟩γ holds in M, q if there exists a general strategy sA for agents A that ensures γ on all outcome paths starting from the epistemic class of q [Alur et al., 2002; Schobbens, 2004]. Analogously, the NatATL formula ⟨⟨A⟩⟩≤k γ holds in M, q if there is a natural strategy sA such that (i) sA ensures γ on all outcome paths from the epistemic class of q, and (ii) compl (sA) ≤ k [Jamroga et al., 2019b; Jamroga et al., 2019c].

Agent Voter1 : LOCAL: [ Voter1_vote1 , Vot er1_vot e2 ] PERSISTENT : [ Voter1_vote1 , Vot er1_vot e2 ] INITIAL : [ ] i n i t q0 vo t e r 1vo t e1 : q0 -> q1 [ Vot er1_vot e1 :=1] sha r ed [ 2 ] gv_1_Voter1 [ gv_1_Voter1 ] : q1 [ Vot er1_vot e1 ==1] -> q2 vo t e r 1vo t e2 : q0 -> q1 [ Vot er1_vot e2 :=1] sha r ed [ 2 ] gv_2_Voter1 [ gv_2_Voter1 ] : q1 [ Vot er1_vot e2 ==1] -> q2 sha r ed [ 2 ] ng_Voter1 [ ng_Voter1 ] : q1 -> q2 sha r ed [ 2 ] pun_Voter1 [ pn_Voter1 ] : q2 -> q3 sha r ed [ 2 ] npun_Voter1 [ pn_Voter1 ] : q2 -> q3

4 Scenarios

We will evaluate our tool on two scalable voting scenarios.

Simple Voting. A simple scalable benchmark is provided by the Asynchronous Simple Voting scenario [Jamroga et al., 2019a]. The system consists of k voters and a single coercer. The NatSTV code specifying the behavior of a voter is shown in Figure 1. The voter first casts their vote, then decides whether to share its value with the coercer. Finally, the voter waits for the coercer's decision to either punish or refrain from punishment. The coercer has two actions available per voter: to punish the voter or to refrain from punishment, resulting in 2k actions in total.

The model contains the following propositional variables: votei,j, indicating whether voter i has voted for candidate j; puni, indicating whether voter i was punished; finishi, indicating whether voter i has completed the voting process and interactions with the coercer.

vVote. The second benchmark is based on a real-life voting protocol, namely the vVote system [Culnane et al., 2015] that was used for the 2014 election in Victoria, Australia. We refer to [Ryan, 2010] and [Jamroga et al., 2021a] for the details of the protocol and the formal model.

5 Technology

NatSTV performs explicit-state model checking, where the global states and transitions of the model are explicitly stored in the memory during the verification process. Users can load and parse the input specification from a text file that defines the modules, which are local automata representing the agents. The generated models and verification results are displayed in an intuitive web-based graphical interface. The verification algorithms are implemented in C++, while the GUI is developed in Typescript using the Angular framework.

NatSTV executes depth-first strategy synthesis from the initial state. During this process, it evaluates whether each new action can extend the existing partial strategy without contradicting prior decisions. Upon completion, the strategy is expressed as a set of boolean conditions involving all agent variables. The tool then optimizes this representation by eliminating redundant variables and conditions, significantly reducing the complexity of the strategy.

6 Experimental Evaluation

6.1 Configuration of the Experiments

The experiments have been conducted on a computer with 8core AMD Ryzen 7 5700X3D running at 3.20 GHz, 64 GB

RAM and a 64-bit Linux operating system. The algorithms were implemented in C++. All execution times are reported in seconds, with the timeout set to 2 hours.

6.2 Simple Voting

For Simple Voting, we verified the following properties:

Formula ϕ1 expresses the undesirable property of strategic punishment, i.e., the coercer can ensure that, whenever his interaction with the voter i concludes and the voter has disobeyed and voted for candidate j, the coercer can punish the voter for that. Formula ϕ2 captures the desirable property of strategic anonymity, i.e., the voter can ensure that the coercer will never know that she has voted for candidate j. Finally, ϕ3 denotes strategic coercion resistance, i.e., the voter can always vote for candidate j without the coercer knowing it. We used j = 2 and i = 1 in all experiments, except for ϕ1 where i = k was used. The experimental results, scaled by the number of voter agents, are presented in Table 1. The natural strategy found by NatSTV for ϕ3 is given below:

Table 1 includes the following columns: scalability parameter (the number of voter agents); model generation time; synthesis time for general strategies and natural strategies; complexity of the synthesized natural strategy without and with optimization. The results demonstrate that the natural strategy synthesis requires approximately the same time as the synthesis of general strategies. The optimization of the natural strategy, although relatively straightforward, significantly reduces its complexity.

Moreover, depending on the agent and the formula, the complexity of the natural strategy may not increase with the number of agents in the system. This occurs for voter strategies, as their strategy is unaffected by other agents, unlike the coercer, who must adapt his choices depending on with whom he currently interacts.

6.3 vVote

For vVote, we consider the following properties:

Formula ϕ4 expresses the desirable property of voter verifiability, indicating that the voter can verify the correctness of her vote on the web bulletin board. Then, ϕ5 represents the undesirable property of strategic coercion, stating that the coercer with the support of the voter can ensure that the voter votes for the first candidate and coercer will know about that. The experimental results, scaled by the number of voter agents, are presented in Tables 2 and 3.

The results show a similar pattern as in the Simple Voting scenario. The natural strategy synthesis requires approximately the same time as the standard strategy synthesis. The reduction of the natural strategy significantly simplifies the strategy. Moreover, the complexity of the natural strategy varies only slightly with the number of agents in the system.

7 Usage

The tool can be accessed at stv.cs-htiew.com. A video demonstration of the tool is available at jmp.sh/AiRcVLmH. Sample specifications are available at stv-docs.cs-htiew.com. The current version of NatSTV offers the following features:

• Generate and visualize the composition of a set of modules into a global multi-agent model;
• Provide local specifications for modules and compute the global specification as their conjunction;
• Display the verification results, including relevant truth values and the winning natural strategy (if one exists).

8 Conclusions

We introduce NatSTV, a novel extension in the STV model checking suite for the synthesis and verification of natural strategies. The experiments indicate that verifying natural strategies with NatSTV yields performance comparable to model checking standard strategic properties. Consequently, we obtain an important new functionality with minimal impact on the complexity and performance of the suite.

Acknowledgments

The work has been supported by NCBR Poland and FNR Luxembourg under the PolLux/FNR-CORE project SpaceVote (POLLUX-XI/14/SpaceVote/2023 and C22/IS/17232062/SpaceVote). For the purpose of open access, and in fulfilment of the grant agreement, the authors have applied CC BY 4.0 license to any Author Accepted Manuscript version arising from this submission.