Y. Abd-alrahman, R. De-nicola, and M. Loreti, A calculus for collective-adaptive systems and its behavioural theory. Information and Computation, p.268, 2019.

,

J. Aspnes and E. Ruppert, An Introduction to Population Protocols, Middleware for Network Eccentric and Mobile Applications, pp.97-120, 2009.

R. L. Axtell, J. M. Epstein, J. S. Dean, G. J. Gumerman, A. C. Swedlund et al., Population growth and collapse in a multiagent model of the Kayenta Anasazi in Long House Valley, Proceedings of the National Academy of Sciences, vol.99, issue.3, pp.7275-7279, 2002.

A. Baeza and M. A. Janssen, Modeling the decline of labor-sharing in the semidesert region of Chile, Regional Environmental Change, vol.18, issue.4, pp.1161-1172, 2018.

,

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, Symbolic model checking without BDDs, 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), vol.1579, pp.193-207, 1999.

M. Blondin, J. Esparza, and S. Jaax, Peregrine: A Tool for the Analysis of Population Protocols, 30th International Conference on Computer Aided Verification (CAV), vol.10981, pp.604-611, 2018.

R. H. Bordini, L. A. Dennis, B. Farwer, and M. Fisher, Automated verification of multi-agent programs, 23rd International Conference on Automated Software Engineering (ASE), pp.69-78, 2008.

H. Y. Chen, C. David, D. Kroening, P. Schrammel, and B. Wachter, Synthesising interprocedural bit-precise termination proofs, 30th International Conference on Automated Software Engineering (ASE), pp.53-64, 2015.

E. Clarke, D. Kroening, and F. Lerda, A tool for checking ANSI-C programs, 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.168-176, 2004.

R. De-nicola, L. Di-stefano, and O. Inverso, Multi-agent systems with virtual stigmergy, Science of Computer Programming, vol.187, 2020.

R. De-nicola, T. Duong, O. Inverso, and F. Mazzanti, Verifying properties of systems relying on attribute-based communication, ModelEd, TestEd, TrustEd. LNCS, vol.10500, pp.169-190, 2017.

R. De-nicola and F. W. Vaandrager, Action versus state based logics for transition systems, Semantics of Systems of Concurrent Processes, vol.469, pp.407-419, 1990.

J. D. Farmer and D. Foley, The economy needs agent-based modelling, Nature, vol.460, issue.7256, pp.685-686, 2009.

M. Y. Gadelha, F. R. Monteiro, J. Morse, L. C. Cordeiro, B. Fischer et al., ESBMC 5.0: An industrial-strength C model checker, 33rd International Conference on Automated Software Engineering (ASE), pp.888-891, 2018.

,

H. Garavel, F. Lang, and R. Mateescu, Compositional verification of asynchronous concurrent systems using, CADP. Acta Informatica, vol.52, issue.4-5, pp.337-392, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01138749

,

H. Garavel, F. Lang, R. Mateescu, and W. Serwe, CADP 2011: A toolbox for the construction and analysis of distributed processes. Software Tools for, Technology Transfer, vol.15, issue.2, pp.89-107, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00715056

H. Garavel, F. Lang, and W. Serwe, From LOTOS to LNT, ModelEd, TestEd, TrustEd. LNCS, vol.10500, pp.3-26, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01621670

H. Garavel, G. Salaün, and W. Serwe, On the semantics of communicating hardware processes and their translation into LOTOS for the verification of asynchronous circuits with CADP, Science of Computer Programming, vol.74, issue.3, pp.100-127, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00381642

,

C. A. Hoare, Communicating Sequential Processes, 1985.

. Iso/iec, LOTOS -A formal description technique based on the temporal ordering of observational behaviour, International Standard, vol.8807, 1989.

D. Kozen, Results on the propositional mu-Calculus, Theoretical Computer Science, vol.27, pp.90125-90131, 1983.

F. Lang, R. Mateescu, and F. Mazzanti, Compositional verification of concurrent systems by combining bisimulations, 3rd World Congress on Formal Methods (FM), vol.11800, pp.196-213, 2019.
URL : https://hal.archives-ouvertes.fr/hal-02295459

F. Lang, R. Mateescu, and F. Mazzanti, Sharp congruences adequate with temporal logics combining weak and strong modalities, 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), vol.12079, pp.57-76, 2020.
URL : https://hal.archives-ouvertes.fr/hal-02555692

A. Lomuscio, H. Qu, and F. Raimondi, MCMAS: An open-source model checker for the verification of multi-agent systems, Software Tools for Technology Transfer, vol.19, issue.1, pp.9-30, 2017.

R. Mateescu and D. Thivolle, A Model Checking Language for Concurrent Value-Passing Systems, 15th International Symposium on Formal Methods (FM), vol.5014, pp.148-164, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00315312

C. Pinciroli, A. Lee-brown, and G. Beltrame, A Tuple Space for Data Sharing in Robot Swarms, 9th International Conference on Bio-inspired Information and Communications Technologies (BICT), pp.287-294, 2015.

J. P. Queille and J. Sifakis, Fairness and related properties in transition systems -A temporal logic to deal with fairness, Acta Informatica, vol.19, pp.195-220, 1983.

K. Sen, M. Viswanathan, and G. Agha, Statistical Model Checking of Black-Box Probabilistic Systems, 16th International Conference on Computer Aided Verification (CAV), vol.3114, pp.202-215, 2004.

J. E. Stiglitz and M. Gallegati, Heterogeneous interacting agent models for understanding monetary economies, Eastern Economic Journal, vol.37, issue.1, pp.6-12, 2011.

M. H. Ter-beek, A. Fantechi, S. Gnesi, and F. Mazzanti, A state/event-based model-checking approach for the analysis of abstract system properties, Science of Computer Programming, vol.76, issue.2, pp.119-135, 2011.

M. Winikoff, Assurance of Agent Systems: What Role Should Formal Verification Play? In: Specification and Verification of Multi-Agent Systems, pp.353-383, 2010.