# Multi-Agent Systems with Information Sharing: Strategies and Model Checking
###### Abstract  
We introduce a prototyping language for multi-agent systems with information sharing, allowing agents to act in parallel and to migrate between distributed locations according to explicit timers. While all agents have access to public information, each agent also has access to private information to decide its next actions. The formal semantics of this language is provided, and an example is used to illustrate multi-agent systems with information sharing. An implementation in the rewriting engine Maude provides the possibility to describe and analyze the evolution of some multi-agent systems. Using the advantage of a strategy module in Maude, we can guide the application of rules, substantially reducing the state space in multi-agent systems with non-deterministic behavior. Given the executable specifications of a multi-agent system, we use the model checking tools of Maude to check various behavioral properties and to detect some behavioral problems. compoitional multi-agent systems; operational semantics; rewriting engine Maude; strategies 2020  
global variables. In our approach, while all agents have access to public information, each agent also has access to private information to decide its next actions. The flexibility of this language is given by the parallel composition of the agents (together with their information); this compositionality provides an easy way of describing large systems starting from small ones and organizing the information of the network better. To capture the system's complex evolution (involving exchange of information between agents), we use labeled transition systems; this allows a rigorous presentation of the behavior of a multi-agent system and a useful way to prove properties about agents. While the introduction of private and public information adds expressiveness, it also increases the complexity of the language. However, this is somehow unavoidable, as we consider a combination that we did not find before in formalisms defined for modeling multi-agent systems: communication, migration, time, and private/public information that can be accessed to perform tests. In order to illustrate the syntax and semantics of our language, and also motivate the multi-agent systems with information sharing, we consider an example in which agents communicate and share information, but also migrate between distributed locations according to explicit timers. A scenario is assumed in which a student finished their lectures at the university and searches for available transportation in order to go home. In front of the university, there are two stations: one for buses and the other for taxis; thus, in order to reach their home location, the student can choose between a bus and a cab. The student has to take into account some information to decide their means of transportation: the costs, the duration of migration, the availability, and the established priority between the transportation choices. The difference between the buses and the cabs is that the buses use a predetermined known scheduler to move between locations, while the cabs move only on demands by clients; note that the bus schedule is available as public information at each location and is updated at each tick. Several tools for performing simulations and model checking for real-time systems are available, e.g., Uppaal [12], PRISM [13], and MCMAS [14]. However, none of these tools are able to model every feature of our approach. For this reason, we provide an implementation in the rewriting engine Maude 3 to observe that the multi-agent systems evolve as desired. As expected, increasing the number of agents, their delays, and the amount of stored information, the size of the system state space grows exponentially. Using this implementation, we emphasize how various strategies can significantly decrease the state space of the systems by controlling the application of the rules and the evolution of information in such highly nondeterministic and concurrent systems.