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) exacerbates these challenges, requiring advanced tools for efective verification. Existing tools like MCMAS and STV face limitations in modularity, flexibility, and usability. This paper is based on VITAMIN (VerIfica Tion of A MultI-ageNt 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.
CEUR ceur-ws.org
Verifying software and hardware systems is challenging due to their complexity and size, often
making exhaustive verification impractical without abstraction or optimisation. This
complexity 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) [
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 [
These challenges are tackled by VITAMIN (VerIfica Tion of A MultI-ageNt system) [
While [
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.
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 sufix of starting at . If is finite, then ( ) = ⟨ 1, … , ⟩ is a tuple, then [] denotes its -th component .
denote its last element || . If
A Concurrent Game Structure (CGS for short) is a tuple = ⟨, , , •
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, = Π the set of all actions; ∈ is the set of tuples of actions, and • ∶ × → (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 if there is a path such that ℎ = ≤ for some ∈ ℕ . We use to denote the set of all histories.
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 [
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.
A Resource Bounded CGS (RB-CGS for short) is a triple = ⟨, , ⟩ where: • ≥ 1 is a natural number (the number of resources types); • ∶ × → ℕ a vector in ℕ .
is a function associating to any state and action , a cost (, ) , that is
As in [
Strategies are defined in the standard way as follows. ∈
it holds that ( ≤ )[] = paths whose first element is .
Let be a state and ∈ (, )
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 a [] . We denote with (, ) the set of all -compatible always; if ∈ ()
; if it is not the case that , ⊧ (denoted ,
⊧ )̸ ; if , ⊧ and , ⊧
; b⟩⟩ X if there is a b-consistent strategy for the coalition such that for every path ∈ (, ) we have that ,
2 ⊧ ; path ∈ (, ) and for every ≥ 1 , we have that , ⊧ ; b⟩⟩ G if there is a b-consistent strategy for the coalition such that for every • , ⊧ ⊤ • , ⊧ • , ⊧ ¬ • , ⊧ ∧ • , ⊧ ⟨⟨ • , ⊧ ⟨⟨ . The cost of at is given by: (, ) = ∑ ( =1 ∑ (, []) ∈ , ( ≤ )) ≤ b
Let be a strategy for the coalition , = 1, a1, 2, … be a path in (, say that is b-consistent when for each natural number ≥ 1 , we have that: ), and b ∈ ℕ . We 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.
Given a RB-CGS , a state of , and a formula , the satisfaction relation , ⊧ is inductively defined on the structure of as follows: • , ⊧ ⟨⟨ b⟩⟩ U if 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 if , ⊧ .
In [
Theorem 1 ([
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 [
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 difering 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).
(|, ) 5 (, ) (, ) , 6 1 (ℎ, ) (|, ) (, ) (, ) (, ) (, ) (ℎ, ) (, ⋆) 3 4 (, ) , (, ) ∅ 2 (⋆, ⋆) (ℎ, ) (, ) (, ) (, ) 2 (, ) (|, ) (⋆, ) (⋆, ) (⋆, ) , 7 (, ) (, ) ∅ 1 (⋆, ⋆) 8 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 suficient 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: ( ) = ℎ ,
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. 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 diferent 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 diferent 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 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.
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 diferent 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 diferent 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 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.
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.
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) i 7-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 1 2 2
Bounds
b1 = 5, b2 = 1 b1 = 2, b2 = 2
Result ⊥ ⊤ ⊥
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.
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.