A contribution to the formal checking of multi-agents systems

The modelling of computing systems using the Multi Agents Systems (MAS) approach nowadays is a method present in the majority of the industry branches: telecommunication, internet, transport, energy, health, etc. So, it is crucial to have rigorous, automatic and effective design and checking methods to ensure these systems development. Our project takes place in the MAS checking scope using the model-checking formal analysis. Although several similar works have been achieved but the absence of a consensus method of formal specification and checking, they all remain incomplete and not general because of the dynamics of this systems type. The main objective of our project is the contribution study of the rewriting logic formalism to the verification of a suitable properties set for the concurrent agents based systems. This work ispractically accomplished with LTL analysis tool of Maude environment.