Hands-on VITAMIN: A Compositional Tool for Model Checking of Multi-Agent Systems Angelo Ferrando1,∗,† , Vadim Malvone2,† 1 University of Modena and Reggio Emilia, Italy 2 Télécom Paris, Institut Polytechnique de Paris, France Abstract Verifying software and hardware systems is challenging due to their complexity, often making exhaustive verification impractical. Transitioning from monolithic systems to Multi-Agent Systems (MAS) exacer- bates these challenges, requiring advanced tools for effective verification. Existing tools like MCMAS and STV face limitations in modularity, flexibility, and usability. This paper is based on VITAMIN (V erI ficaT ion of A M ultI -ageN t system), a formal verification framework designed to support various logic and model formalisms while providing a user-friendly experience. Specifically, we apply VITAMIN to a case study in the robotics domain, focusing on an extension of Alternating-time Temporal Logic with resource bounds (RB-ATL). Through this case study, we demonstrate VITAMIN ’s ability to guide end-users in the formal verification process and report experimental results to showcase its usability and feasibility. Keywords Model Checking, Multi-Agent Systems, Verification Tools 1. Introduction Verifying software and hardware systems is challenging due to their complexity and size, often making exhaustive verification impractical without abstraction or optimisation. This complex- ity demands deep expertise in formal methods, limiting the usability of formal verification techniques in real-world development. One of the most representative approaches to achieve exhaustive formal verification is Model Checking (MC) [1]. Transitioning from monolithic systems to Multi-Agent Systems (MAS) exacerbates these challenges. In fact, as monoloithic systems, MAS face similar verification challenges but with added complexity due to agents’ rationality and their interactions. Formal verification for MAS relies heavily on tools like MCMAS [2] and STV [3]. MCMAS is widely used for strategic verification of MAS due to its early development and foundational role in research. However, it has issues hindering broader adoption, including a hard-coded verification process and a lack of modularity, which affects the separation of different logics and models. Despite various extensions, MCMAS lacks transparent extension capabilities for new logics and models, causing maintainability issues. Additionally, its execution can be challenging as it requires additional WOA 2024: 25th Workshop “From Objects to Agents”, July 8-10, 2024, Forte di Bard (AO), Italy ∗ Corresponding author. † These authors contributed equally. Envelope-Open angelo.ferrando@unimore.it (A. Ferrando); vadim.malvone@telecom-paris.fr (V. Malvone) Orcid 0000-0002-8711-4670 (A. Ferrando); 0000-0001-6138-4229 (V. Malvone) © 2022 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR ceur-ws.org Workshop ISSN 1613-0073 Proceedings tools like Eclipse for installation and lacks comprehensive external documentation. These limitations stem from its primary function as a research tool. STV is designed for specific verification goals but lacks the compositional nature and flexibility to support different logics or models for MAS verification. It also lacks comprehensive documentation to assist users and developers. Both MCMAS and STV require a strong background in formal methods, making them challenging for non-expert users. In summary, both tools lack modularity and usability. These challenges are tackled by VITAMIN (V erI ficaT ion of A M ultI -ageN t system) [4], a new formal verification framework for MAS. VITAMIN aims to be highly compositional, supporting various logic and model formalisms, while also providing a user-friendly experience for both developers and end-users. VITAMIN aims to generalise MAS verification without being tied to specific logic or model formalisms. It achieves compositionality through its design, minimising assumptions about the types of logics and models used. The user experience is enhanced to guide the entire verification process. VITAMIN is still under development, but its compositional nature allows for straightforward extension of its components by external developers. While [4] discusses the architecture and engineering of VITAMIN , this paper focuses on applying VITAMIN to a interesting case study in the robotics domain. Specifically, we aim to demonstrate how VITAMIN can guide the end-user in the formal verification of a MAS. Although VITAMIN is general and supports various formal logics, to improve readability and better explain its process, we focus on an extension of Alternating-time Temporal Logic (ATL) [5] with resource bounds, called RB-ATL [6]. Using this logic, we present step-by-step how VITAMIN can assist the end-user in verifying an extension of the Curiosity [7] rover case study against formal specifications expressed through RB-ATL. In addition to detailing the steps required by VITAMIN to achieve formal verification, we also report experimental results from the case study. The goal of this work is to demonstrate the high usability of VITAMIN and its feasibility in an application to a robotic case study. The structure of the paper is as follows: Section 2 introduces all the preliminaries necessary to understand the content of the paper. Section 3 presents the Curiosity rover case study. Section 4 details the step-by-step use of VITAMIN to support the end-user in the formal verification of the case study. Finally, Section 5 concludes the paper and points to future directions. 2. Preliminaries Let us fix some notation and terminology that will be used in the following. If 𝑋 is a set and 𝑌 ⊆ 𝑋, we denote by 𝑌 the complementary set 𝑋 ⧵ 𝑌 of 𝑌 in 𝑋. If 𝜋 is a sequence, we denote by |𝜋| its length and, given 𝑖 ≤ |𝜋|, we let 𝜋𝑖 denote the 𝑖-th element of 𝜋, 𝜋≤𝑖 the prefix 𝜋1 , … , 𝜋𝑖 of 𝜋 and 𝜋≥𝑖 the suffix of 𝜋 starting at 𝜋𝑖 . If 𝜋 is finite, then 𝑙𝑎𝑠𝑡(𝜋) denote its last element 𝜋|𝜋| . If 𝛼 = ⟨𝑥1 , … , 𝑥𝑛 ⟩ is a tuple, then 𝛼[𝑖] denotes its 𝑖-th component 𝑥𝑖 . Definition 1. A Concurrent Game Structure (CGS for short) is a tuple 𝔊 = ⟨𝐴𝑝, 𝐴𝑔, 𝑆, 𝑠𝐼 , {𝑎𝑐𝑡𝑖 }𝑖∈𝐴𝑔 , 𝑃, 𝑡⟩ such that: • 𝐴𝑝 is a non-empty set of atomic propositions; • 𝐴𝑔 = {1, … , 𝑛} is a finite set of agents; • 𝑆 is a non-empty set of states and 𝑠𝐼 ∈ 𝑆 is the initial state; • for any 𝑖 ∈ 𝐴𝑔, 𝑎𝑐𝑡𝑖 is a set of actions, 𝐴𝐶𝑇 = Π𝑖∈𝐴𝑔 𝑎𝑐𝑡𝑖 is the set of tuples of actions, and 𝑎𝑐𝑡 = ⋃𝑖∈𝐴𝑔 𝑎𝑐𝑡𝑖 the set of all actions; • 𝑃 ∶ 𝐴𝑔 × 𝑆 → (2𝑎𝑐𝑡 ⧵ ∅) is the protocol function that associates to any agent 𝑖 and state 𝑠 a non-empty subset of 𝑎𝑐𝑡𝑖 representing the actions that are available for 𝑖 at 𝑠. We impose that the idle action ⋆ always belong to 𝑃(𝑖, 𝑠) for any 𝑖; • 𝑡 ∶ 𝑆 × 𝐴𝐶𝑇 → 𝑆 is the transition function, that is given a state 𝑠 and a tuple of actions a (where ∀𝑖, a[𝑖] ∈ 𝑃(𝑖, 𝑠)) such function outputs a state 𝑠 ′; • 𝐿 ∶ 𝑆 → 2𝐴𝑝 is the labeling function associating to any state 𝑠 a set of atomic propositions; such set can be empty and represents the set of proposition that are true at 𝑠. If 𝐶 is a coalition (i.e., a set of agents) and 𝑠 is a state a C-action available at 𝑠 is a tuple 𝛼 whose length is |𝐴𝑔| and such that 𝛼𝑖 ∈ 𝑃(𝑠, 𝑖) for each 𝑖 ∈ 𝐶 and for each 𝑗 ∈ 𝐶, 𝛼𝑗 = #𝑗 , where #𝑗 is a fixed symbol used as placeholder for an arbitrary action of player 𝑗. We denote by 𝐴𝑐𝑡(𝐶, 𝑠) the set of all C-actions at 𝑠. If 𝛼 ∈ 𝐴𝑐𝑡(𝐶, 𝑠) and 𝛽 ∈ 𝐴𝑐𝑡(𝐶, 𝑠) then 𝛼 ⋅ 𝛽 denotes the unique joint action a ∈ 𝐴𝑐𝑡(𝐴𝑔, 𝑠) such that a[𝑖] = 𝛼[𝑖] for each 𝑖 ∈ 𝐶 and a[𝑗] = 𝛽[𝑗] for each 𝑗 ∈ 𝐶. We denote by 𝐴𝑐𝑡(𝐶, 𝑆) the set ⋃𝑠∈𝑆 𝐴𝑐𝑡(𝐶, 𝑠). A path 𝜌 is an infinite alternated sequence 𝑠1 , a1 , 𝑠2 , … of states and tuples in 𝐴𝐶𝑇 such that for all 𝑖 ≥ 1, 𝑡(𝑠𝑖 , a𝑖 ) = 𝑠𝑖+1 . If 𝜌 is a path, we denote by 𝜌 𝑆 the sub-sequence of 𝜌 only containing states. If ℎ ∈ 𝑆 + is a finite sequence of states, we say that ℎ is a history iff there is a path 𝜌 such that ℎ = 𝜌≤𝑖 𝑆 for some 𝑖 ∈ ℕ. We use 𝐻 to denote the set of all histories. 2.1. Resource Bounded ATL In many multi-agent systems, agents are resource-bounded, in the sense that they require resources in order to act. To formalise such notion, in [6] the authors introduced Resource Bounded ATL (RB-ATL for short). RB-ATL is a variant of ATL in which strategic formulae are decorated with bound, i.e., natural numbers vectors of finite size. The intended meaning of a formula ⟨⟨𝐶 b ⟩⟩ 𝜓 of RB-ATL can be expressed as the coalition of agents 𝐶 has a strategy to achieve the objective 𝜓 whose cost does not surpass b. We now recall the syntax and semantics of RB-ATL. Definition 2. Formulae of RB-ATL are defined by the following grammar: 𝜑 ∶∶= ⊤ ∣ 𝑝 ∣ ¬𝜑 ∣ 𝜑 ∧ 𝜑 ∣ ⟨⟨𝐶 b ⟩⟩ X 𝜑 ∣ ⟨⟨𝐶 b ⟩⟩ G 𝜑 ∣ ⟨⟨𝐶 b ⟩⟩ 𝜑 U 𝜑 where 𝑝 ∈ 𝐴𝑝, 𝐶 ⊆ 𝐴𝑔, b is any bound, ⟨⟨𝐶 b ⟩⟩ is the strategic operator, X is the next operator, G is the globally operator, and U is the until operator. We can derive the boolean connectives ⊥, ∨, and → as usual. We define ⟨⟨𝐶 b ⟩⟩ F 𝜑 as ⟨⟨𝐶 b ⟩⟩ ⊤ U 𝜑. We will use 𝜑, 𝜓 , 𝜃, etc., to denote arbitrary formulae. Formulae of RB-ATL are interpreted over RB-CGSs. These are CGSs in which a cost (a natural number vector) is associated to any agent action at any state. The formal definition follows. Definition 3. A Resource Bounded CGS (RB-CGS for short) is a triple 𝔐 = ⟨𝔊, 𝑟, 𝒞 ⟩ where: • 𝔊 is a CGS as in Definition 1; • 𝑟 ≥ 1 is a natural number (the number of resources types); • 𝒞 ∶ 𝑆 × 𝑎𝑐𝑡 → ℕ𝑟 is a function associating to any state 𝑠 and action 𝑎, a cost 𝒞 (𝑠, 𝑎), that is a vector in ℕ𝑟 . As in [6] we impose that any agent at any state has at its disposal the idle action ⋆ and that the cost of such action is always 0. Strategies are defined in the standard way as follows. Definition 4. A strategy for a coalition of agents 𝐶 is a function 𝜎𝐶 ∶ 𝐻 → 𝐴𝑐𝑡(𝐶, 𝑆) mapping a history ℎ to a joint action 𝛼 ∈ 𝐴𝑐𝑡(𝐶, 𝑙𝑎𝑠𝑡(ℎ)). A path 𝜌 = 𝑠1 , a1 , 𝑠2 … is compatible with a joint strategy 𝜎𝐶 if for every 𝑖 ≥ 1 and every 𝑘 ∈ 𝐶 it holds that 𝜎𝐶 (𝜌≤𝑖𝑆 )[𝑘] = a [𝑘]. We denote with 𝑜𝑢𝑡(𝑠, 𝜎 ) the set of all 𝜎 -compatible 𝑖 𝐶 𝐶 paths whose first element is 𝑠. Let 𝑠 be a state and 𝛼 ∈ 𝐴𝑐𝑡(𝐶, 𝑠). The cost of 𝛼 at 𝑠 is given by: 𝑐𝑜𝑠𝑡(𝑠, 𝛼) = ∑ 𝒞 (𝑠, 𝛼[𝑖]) 𝑖∈𝐶 Let 𝜎𝐶 be a strategy for the coalition 𝐶, 𝜌 = 𝑠1 , a1 , 𝑠2 , … be a path in 𝑜𝑢𝑡(𝑠, 𝜎𝐶 ), and b ∈ ℕ𝑟 . We say that 𝜌 is b-consistent when for each natural number 𝑛 ≥ 1, we have that: 𝑛 𝑆 )) ≤ b ∑ 𝑐𝑜𝑠𝑡(𝑠𝑘 , 𝜎𝐶 (𝜌≤𝑘 𝑘=1 A strategy 𝜎𝐶 for a coalition 𝐶 is b-consistent whenever, for every state 𝑠, given any 𝜌 ∈ 𝑜𝑢𝑡(𝑠, 𝜎𝐶 ), 𝜌 is b-consistent. We now define the semantic interpretation of RB-ATL formulae. Definition 5. Given a RB-CGS 𝔐, a state 𝑠 of 𝔐, and a formula 𝜑, the satisfaction relation 𝔐, 𝑠 ⊧ 𝜑 is inductively defined on the structure of 𝜑 as follows: • 𝔐, 𝑠 ⊧ ⊤ always; • 𝔐, 𝑠 ⊧ 𝑝 iff 𝑝 ∈ 𝐿(𝑠); • 𝔐, 𝑠 ⊧ ¬𝜓 iff it is not the case that 𝔐, 𝑠 ⊧ 𝜓 (denoted 𝔐, 𝑠⊧𝜓̸ ); • 𝔐, 𝑠 ⊧ 𝜓 ∧ 𝜃 iff 𝔐, 𝑠 ⊧ 𝜓 and 𝔐, 𝑠 ⊧ 𝜃; • 𝔐, 𝑠 ⊧ ⟨⟨𝐶 b ⟩⟩ X 𝜓 iff there is a b-consistent strategy 𝜎𝐶 for the coalition 𝐶 such that for every path 𝜌 ∈ 𝑜𝑢𝑡(𝑠, 𝜎𝐶 ) we have that 𝔐, 𝜌2𝑆 ⊧ 𝜓; • 𝔐, 𝑠 ⊧ ⟨⟨𝐶 b ⟩⟩ G 𝜓 iff there is a b-consistent strategy 𝜎𝐶 for the coalition 𝐶 such that for every path 𝜌 ∈ 𝑜𝑢𝑡(𝑠, 𝜎𝐶 ) and for every 𝑖 ≥ 1, we have that 𝔐, 𝜌𝑖𝑆 ⊧ 𝜓; • 𝔐, 𝑠 ⊧ ⟨⟨𝐶 b ⟩⟩ 𝜓 U 𝜃 iff there is a b-consistent strategy 𝜎𝐶 for the coalition 𝐶 such that for every path 𝜌 ∈ 𝑜𝑢𝑡(𝑠, 𝜎𝐶 ) there exists a 𝑗 ≥ 1 such that 𝔐, 𝜌𝑗𝑆 ⊧ 𝜃 and for every 1 ≤ 𝑖 < 𝑗 we have that 𝔐, 𝜌𝑖𝑆 ⊧ 𝜓. We write 𝔐 ⊧ 𝜑 and we say that 𝔐 satisfies 𝜑 iff 𝔐, 𝑠𝐼 ⊧ 𝜑. In [6] the authors claim that the model-checking problem for RB-ATL can be solved in time that is linear on the size of the model and exponential in the number 𝑟 of resource bounds. We report the exact statement of the Theorem. Theorem 1 ([6]). Given a finite RB-CGS 𝔐 and a formula 𝜑, there is an algorithm that computes [[𝜑]]𝔐 which runs in O(|𝔐|, |𝜑|2𝑟+1 ) where |𝔐| is the size of the RB-CGS and 𝑟 is its the number of resources. 3. Case study The Curiosity rover stands as one of the most sophisticated systems ever deployed for planetary exploration missions. Its primary goals are to capture image data and gather soil and rock samples. Unlike the original model [7], in this scenario, the rover is equipped with autonomous decision-making capabilities, as described in [8]. However, contrary to the scenario in [8], we assume the rover operates with perfect information but factor in the resources necessary to accomplish the mission. We simulate an inspection mission where the Curiosity rover patrols a topological map of the Martian surface. In Figure 1, we illustrate the model 𝔐 that describes a sample mission for the rover. The mission begins with the rover in state 𝑠𝐼 , where it must execute a setup action (𝑐ℎ𝑘) that involves checking one of the rover’s three main components: the arm (𝑐𝑎), the mast (𝑐𝑚), or the wheels (𝑐𝑤). To conserve time and energy, the mechanic (the entity responsible for performing the setup checks and making any necessary adjustments) conducts only one setup operation per mission. Specifically, checking the arm requires 5 units of time and 3 units of energy, inspecting the mast takes 2 units of time and 4 units of energy, and examining the wheels consumes 3 units of time and 5 units of energy. These varying requirements are due to the differing complexities of each action. The rover must validate the setup operation. If, in the initial state, the mechanic chooses to check the arm, denoted as 𝑐𝑎, then in the subsequent state, 𝑠1 , the rover needs to perform the 𝑐𝑎 action to proceed from 𝑠1 . The same logic applies to the other two setup actions. After the selection, the mechanic can either choose to check and potentially correct the component (action 𝑜𝑘) or decline the operation (action 𝑛𝑜𝑘). In the former case, the rover can continue the mission, whereas in the latter, the mission ends with an error. If the mechanic collaborates, the rover can begin the mission. We denote the state where the rover is at the base camp as 𝑠4 . The objective is for the rover to move from its initial position, take a picture of a sample rock on Mars, and then return to the starting position. Specifically, from state 𝑠4 , the rover can decide to move left (𝐿) to state 𝑠6 or right (𝑅) to state 𝑠7 . In either of these states, the rover can take a photo of a sample rock (action 𝑚𝑝). Following this step, the rover must conclude the mission by returning to the base camp. To do this, it needs to perform the complementary move action to return to the previously visited state (𝑅 from 𝑠6 and 𝐿 from 𝑠7 ). (𝑖, ⋆) 𝑠𝑝 𝑠𝐼 (𝑐ℎ𝑘, 𝑐𝑎) (𝑐ℎ𝑘, 𝑐𝑤) (𝑐ℎ𝑘, 𝑐𝑚) 𝑐𝑝 𝑐𝑝 (𝑐𝑚|𝑐𝑤, 𝑜𝑘) 𝑠1 𝑠2 (𝑐𝑎|𝑐𝑚, 𝑜𝑘) (⋆, 𝑛𝑜𝑘) 𝑐𝑝 (⋆, 𝑛𝑜𝑘) 𝑠3 (⋆, 𝑛𝑜𝑘) ∅ (𝑐𝑎|𝑐𝑤, 𝑜𝑘) (𝑐𝑤, 𝑜𝑘) 𝑒1 (𝑐𝑚, 𝑜𝑘) (𝑐𝑎, 𝑜𝑘) (⋆, ⋆) 𝑜𝑐,𝑟𝑚 𝑠4 (𝐿, 𝑖) (𝑅, 𝑖) (𝑖, 𝑖) (𝑅, 𝑖) (𝐿, 𝑖) (𝑚𝑝, 𝑖) (𝑚𝑝, 𝑖) 𝑝𝑙 𝑟𝑝,𝑖𝑝 ∅ 𝑟𝑝,𝑖𝑝 𝑝𝑟 (𝐿, 𝑖) 𝑒2 (𝑅, 𝑖) 𝑠8 𝑠5 (𝑖, 𝑖) 𝑠6 𝑠7 (𝑖, 𝑖) (⋆, ⋆) Figure 1: The rover’s mission where 𝑖 stands for idle and ⋆ for any action. The atoms have the following acronyms: 𝑠𝑝 as starting position, 𝑐𝑝 as check phase, 𝑜𝑐 as ok check phase, 𝑟𝑚 as ready to mission, 𝑟𝑝 as ready to make a picture, 𝑖𝑝 as in position, 𝑝𝑙 as picture left, and 𝑝𝑟 as picture right. Given the model 𝑀, we can define several specifications. For example, the ATL specification that describes the rover mission is 𝜑1 = ⟨⟨𝑟𝑜𝑣𝑒𝑟⟩⟩ 𝐹 ((𝑜𝑐 ∧ 𝑟𝑚) ∧ ⟨⟨𝑟𝑜𝑣𝑒𝑟⟩⟩ 𝐹 ((𝑝𝑙 ∨ 𝑝𝑟) ∧ ⟨⟨𝑟𝑜𝑣𝑒𝑟⟩⟩ 𝐹 (𝑜𝑐 ∧ 𝑟𝑚))) In words, this formula means that there exists a strategy for the rover such that it will eventually be ready to start the mission, can take a picture of a sample rock, and can return to the base camp. In the previous formula, we assume that the mechanic may choose not to cooperate. In this scenario, it becomes impossible for the rover to complete the mission. Thus, the formula 𝜑1 is false in the model 𝔐. However, if we assume the mechanic cooperates (i.e., the mechanic checks a component and corrects it if necessary via the action 𝑜𝑘), we can rewrite the specification as an RB-ATL formula: 𝜑2 = ⟨⟨𝑟𝑜𝑣𝑒𝑟, 𝑚𝑒𝑐ℎ𝑎𝑛𝑖𝑐 ⟨b1 ,b2 ⟩ ⟩⟩ 𝐹 ((𝑜𝑐 ∧ 𝑟𝑚) ∧ ⟨⟨𝑟𝑜𝑣𝑒𝑟⟩⟩ 𝐹 ((𝑝𝑙 ∨ 𝑝𝑟) ∧ ⟨⟨𝑟𝑜𝑣𝑒𝑟⟩⟩ 𝐹 (𝑜𝑐 ∧ 𝑟𝑚))) where b1 sets the resource bound for time, while b2 sets the resource bound for energy. If b1 and b2 are sufficient for the mechanic to select the actions necessary to achieve its strategic objectives, then the rover has a strategy to satisfy the formula by relying on the mechanic’s cooperation, that is 𝔐 satisfies 𝜑2 . In fact, a simple strategy 𝜎 can be defined as follows: 𝜎 (𝑠𝐼 ) = 𝑐ℎ𝑘, Figure 2: VITAMIN ’s GUI: Step (i) - Number and Names of Agents. 𝜎(𝑠𝐼 𝑠𝑗 ) = 𝑐𝑎, 𝜎 (𝑠𝐼 𝑠𝑗 𝑠𝑘 ) = 𝑐𝑚, 𝜎 (𝑠𝐼 𝑠𝑗 𝑠𝑘 𝑠𝑟 ) = 𝑐𝑤, 𝜎 (𝑠𝐼 𝑠𝑗 𝑠4 ) = 𝐿, 𝜎 (𝑠𝐼 𝑠𝑗 𝑠4 𝑠6 ) = 𝑚𝑝, 𝜎 (𝑠𝐼 𝑠𝑗 𝑠4 𝑠6 𝑠5 ) = 𝑖, and 𝜎(𝑠𝐼 𝑠𝑗 𝑠4 𝑠6 𝑠5 𝑠6 ) = 𝑅, where 𝑗, 𝑘, 𝑟 ∈ {1, 2, 3}. 4. VITAMIN in action In this section, we demonstrate how VITAMIN can be used to verify the previously presented case study. We do this by following all the steps required to build the CGS shown in Figure 1. Note that, in VITAMIN , there are two possible ways to create CGSs. The first method is for expert users and requires the user to upload a properly formatted CGS according to VITAMIN ’s input format. The second method is for non-expert users and allows VITAMIN to guide the user through the CGS creation process in a step-by-step fashion. Agents. The first aspect VITAMIN queries the user about is the number of agents in the MAS. Figure 2 reports a screenshot of VITAMIN ’s GUI. In this step, the user can decide how many agents are in the MAS and which are their names. Considering the rover case study, in this step, we report the presence of two agents, called rover and mechanic, respectively. States. Once the agents have been decided, VITAMIN asks for the states of the CGS. Figure 3 reports this step. In our scenario, according to Figure 1, we have 11 different states, that is the initial state 𝑠𝐼 , the normal states 𝑠1 to 𝑠8 , and the error states 𝑒1 and 𝑒2 . Atoms. States may contain atomic propositions, thus, after gathering the states, VITAMIN expects the user to provide the atoms holding in such states. Figure 4 reports this step in VITAMIN ’s GUI. Considering once more the rover case study, in this step we may find 8 different atomic propositions. Labelling. Naturally, atomic propositions make sense when linked to the states of our model. Thus, after gathering the atoms, VITAMIN requires the user to report which atoms hold in which states of the CGS. Figure 5 report this step for the rover case study. Here, we can observe how Figure 3: VITAMIN ’s GUI: Step (ii) - Number and Names of States. Figure 4: VITAMIN ’s GUI: Step (iii) - Number and Names of Atoms. the states are labelled according to Figure 1, where in each state the user can list all the atoms holding in such a state (e.g., in state 𝑠4 the 𝑜𝑐 and 𝑟𝑚 atoms hold). Resources. Since we are talking about CGSs with resources (i.e., RB-CGSs), after populating the model with states and atoms, the user needs to insert the number and names of the resources to be considered in the RB-CGS. Figure 6 reports the corresponding step in VITAMIN ’s interface, where time and energy are listed as the two resources to be considered in the model. Figure 5: VITAMIN ’s GUI: Step (iv) - Labelling. Figure 6: VITAMIN ’s GUI: Step (v) - Number and Names of Resources. Actions. After the agents, states, atoms, and resources have been gathered, VITAMIN continues by asking for the actions to be performed by the agents. Figure 7 reports the list of actions for the rover case study, where we have 10 different actions to be performed by the rover and mechanic agents. Transitions. Once the actions are given, VITAMIN expects the user to insert the transitions amongst the different states of the model. Figure 8 and Figure 9 report a snippet of the transitions of the rover and mechanic agents, respectively. For lack of space, only a subset of the transitions is reported. Note that, thanks to VITAMIN ’s GUI, the user can easily and intuitively insert the actions each agent can perform in a state to reach another state. For instance, in Figure 8, the user can insert that the rover agent can perform the action 𝑐ℎ𝑘 in state 𝑠𝐼 to reach states 𝑠1 , 𝑠2 , and 𝑠3 (as reported in Figure 1). Costs. Last, but not least, to complete all information on the model, VITAMIN asks the user to report the costs of the transitions. Note that, the cost is determined by the actions and the Figure 7: VITAMIN ’s GUI: Step (vi) - Actions. Figure 8: VITAMIN ’s GUI: Step (vii) - Transitions of the rover agent. states such actions are performed into. Figure 10 reports a snippet of the costs introduced in the context of the rover case study. Here, we can see how the costs matches the ones presented in Section 3, when we presented the notion of time and energy. Visualisation. Before concluding with the verification of the properties of interest, VITAMIN allows the user to validate the model created by following the previous steps. In particular, VITAMIN shows the resulting model via its GUI to the user. Figure 9: VITAMIN ’s GUI: Step (vii) - Transitions of the mechanic agent. Figure 10: VITAMIN ’s GUI: Step (viii) - Costs of the transitions. Formula and Verification. Finally, after the model is created and validated by the user, the guided process concludes by asking the user to fill in the formula to verify on the model. In this step, as reported in Figure 11, the user can select the logic to use (in this case RBATL), and insert the formula to verify on the model; in this case, as an example, we reported 𝜑2 with b1 = 5 and b2 = 1. After filling these two fields, VITAMIN runs the corresponding model checking algorithm for the logic and model selected, and returns back to the user the result of the verification. Figure 11: VITAMIN ’s GUI: Step (ix) - Logic and Verification. 4.1. Experimental results Other than showing how VITAMIN can support a user in the definition of a model to verify, we also want to report the experimental results obtained on the verification of the actual rover case study. We tested our tool over the rover’s mission, on a machine with the following specifications: Intel(R) Core(TM) i7-7700HQ CPU @ 2.80GHz, 4 cores 8 threads, 16 GB RAM DDR4. Specifically, we verified formula 𝜑1 and 𝜑2 and reported the results so obtained in Table 1. Formula Bounds Result Time (sec) 𝜑1 - ⊥ 0.003 𝜑2 b1 = 5, b2 = 1 ⊤ 0.082 𝜑2 b1 = 2, b2 = 2 ⊥ 0.024 Table 1 Results of the verification process for different formulas and bounds As we can see, the verification can be concluded within 0.1 seconds. In the case of 𝜑1 , this requires less than 4 milliseconds. For 𝜑2 , the verification time ranges from 0.024 to 0.082 seconds, depending on the values associated with b1 and b2 . Now, we can discuss the outcome of the tool. As discussed in Section 3, 𝜑1 should be false, and in fact our tool returns false. The formula 𝜑2 with enough resources for the mechanic (like b1 = 5 and b2 = 1) is verified in 𝔐, as it is confirmed by our tool; while with less resources (like b1 = 2 and b2 = 2) 𝜑2 is not verified in 𝔐, also confirmed by our tool. These experiments, although limited to the case study presented in this paper, demonstrate the applicability and feasibility of VITAMIN in tackling resource-bound verification of MAS. 5. Conclusions and Future Work In this paper, we presented how VITAMIN can guide the verification of an interesting case study based on the Curiosity rover. We demonstrated how VITAMIN supports the user in all specification phases, including the construction, population, and verification of the CGS against a formal specification. We conducted experiments with VITAMIN and reported the results, confirming its applicability. Furthermore, we evaluated not only the usability of the tool but also its performance in the formal verification of the case study. As a future direction, we plan to further test VITAMIN on more complex case studies and to gather feedback from the MAS community on its usability. This feedback will be used to further improve and extend VITAMIN . References [1] C. Baier, J.-P. Katoen, Principles of model checking, MIT press, 2008. [2] A. Lomuscio, H. Qu, F. Raimondi, MCMAS: an open-source model checker for the verification of multi-agent systems, Int. J. Softw. Tools Technol. Transf. 19 (2017) 9–30. URL: https: //doi.org/10.1007/s10009-015-0378-x. doi:10.1007/S10009- 015- 0378- X . [3] D. Kurpiewski, W. Jamroga, M. Knapik, STV: model checking for strategies under imperfect information, in: E. Elkind, M. Veloso, N. Agmon, M. E. Taylor (Eds.), Proceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems, AAMAS ’19, Montreal, QC, Canada, May 13-17, 2019, International Foundation for Autonomous Agents and Multiagent Systems, 2019, pp. 2372–2374. URL: http://dl.acm.org/citation.cfm? id=3332116. [4] A. Ferrando, V. Malvone, VITAMIN: A compositional framework for model checking of multi- agent systems, CoRR abs/2403.02170 (2024). URL: https://doi.org/10.48550/arXiv.2403.02170. doi:10.48550/ARXIV.2403.02170 . arXiv:2403.02170 . [5] R. Alur, T. A. Henzinger, O. Kupferman, Alternating-time temporal logic, J. ACM 49 (2002) 672–713. URL: https://doi.org/10.1145/585265.585270. doi:10.1145/585265.585270 . [6] N. Alechina, B. Logan, N. H. Nga, A. Rakib, Resource-bounded alternating-time temporal logic, in: W. van der Hoek, G. A. Kaminka, Y. Lespérance, M. Luck, S. Sen (Eds.), 9th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2010), Toronto, Canada, May 10-14, 2010, Volume 1-3, IFAAMAS, 2010, pp. 481–488. URL: https: //dl.acm.org/citation.cfm?id=1838274. [7] NASA, Mars curiosity rover, 2012. URL: https://mars.nasa.gov/msl/home/. [8] A. Ferrando, V. Malvone, Towards the verification of strategic properties in multi-agent systems with imperfect information, in: N. Agmon, B. An, A. Ricci, W. Yeoh (Eds.), Proceed- ings of the 2023 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2023, London, United Kingdom, 29 May 2023 - 2 June 2023, ACM, 2023, pp. 793–801. URL: https://dl.acm.org/doi/10.5555/3545946.3598713. doi:10.5555/3545946.3598713 .