Towards the Combination of Model Checking and Runtime Verification on Multi-Agent Systems

Intelligent systems, such as Multi-Agent Systems (MAS), can be seen as a set of intelligent entities capable of proactively decide how to act to fulfill their own goals. These entities, called generally agents, are notoriously autonomous, i.e., they do not expect input from an user to act, and social, i.e., they usually communicate amongst each other to achieve common goals. Software systems are not easy to trust in general. This is especially true in the case of complex and distributed systems, such as MAS. Because of this, we need verification techniques to verify that such systems behave as expected. More specifically, in the case of MAS, it is relevant to know whether the agents are capable of achieving their own goals, by themselves or by collaborating with other agents by forming a coalition. This is usually referred to as the process of finding a strategy for the agent(s). A well-known formalism for reasoning about strategic behaviours in MAS is Alternating-time Temporal Logic (AT L) [1]. Before verifying AT L specifications, two questions need to be answered: (i) does each agent know everything about the system?