Trainee Project
Title:
Research Assistant in Multi-Agent Technologies
Dates:
2023/06/01 - 2023/11/30
Supervisor(s):
Other supervisor(s):
MCF, LIU Yinling (yinling.liu@univ-lorraine.fr)
, Professeure BRIL-EL HAOUZI Hind (hind.el-haouzi@univ-lorraine.fr)
Description:
Project Title: Formal Verification of Multi-Agent Systems Centred on Humans
Context
Human factors are not sufficiently considered in the design of Manufacturing Control Systems (MCS) [1]. The laboratory CRAN
proposed a meta model of social relationships of agents and employed Multi-Agent Systems (MAS) to describe future MCS [2]. The
laboratory considered the integration of humans into MCS by analysing the interaction mechanisms of agents. This work laid the
foundation for analysing the accessibility, comprehension, and adaptation between humans and systems. The technical platform
TRACILOGIS of CRAN was used to illustrate the feasibility of this formal model. However, the impacts of the proposed social
relationships on the behaviour of MCS are not adequately addressed. The laboratory would like to perform a formal verification of
MAS centred on humans, which illustrates the feasibility of the work from the theoretical aspect. The real-time properties, collision
free, safety, etc., are the major concerns of MCS [5]. Model checking is commonly used for verifying MCS [3-5]. Therefore, the goal
of this project is to be able to formally verify the above-mentioned properties of MCS centred on humans via model checking, in
order to ensure the quality of the design of MCS.
Mission
To achieve the goal of this project, the research assistant will firstly conduct the literature reviews of agent architectures and model
checking of MCS. He/She will then analyse our meta model of social relationships of agents in order to identify the most appropriate
agent architecture and model checking technique. The extension of the chosen agent architecture is potentially needed to accurately
describe the social relationships. This extension possibly necessitates the adaptation of the chosen Multi-Agent Programming
Language (MAPL). In the following, he/she will formalize the model of MCS with the updated MAPL. Next, a model transformer
will be developed to automate the verification process. Finally, a scientific paper will be demanded to conclude his/her work.
Essential requirements
Applicants are expected to have the following:
A strong background in formal verification;
Strong programming skills in Java, C++, C, etc.;
Good communication, excellent technical writing skills, and ability to prioritise work to meet deadlines;
Master degree (or equivalent) in an area pertinent to the subject area in Computer Science or a related field;
The ability to work autonomously in a multi-cultural environment.
How to apply
Applicants should send their applications to LIU Yinling (yinling.liu@univ-lorraine.fr) before 30 April 2023.
All applications must include:
A full CV;
A motivation letter;
Two recommendation letters if possible.
References
[1] El-Haouzi, H. B., & Valette, E. (2021). Human system integration as a key approach to design manufacturing control system for
Industry 4.0: Challenges, barriers, and opportunities. IFAC-PapersOnLine, 54(1), 263-268.
[2] Valette, E. (2022). Toward an anthropocentric approach for intelligent manufacturing systems' control architectures (Doctoral
dissertation, Université de Lorraine).
[3] Wooldridge, M., Fisher, M., Huget, M. P., & Parsons, S. (2002, July). Model checking multi-agent systems with MABLE. In
Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2 (pp. 952-959).
[4] Bordini, R. H., Fisher, M., Visser, W., & Wooldridge, M. (2006). Verifying multi-agent programs by model checking. Autonomous
agents and multi-agent systems, 12(2), 239-256.
[5] Drawel, N., Bentahar, J., Laarej, A., & Rjoub, G. (2022). Formal verification of group and propagated trust in multi-agent systems.
Autonomous Agents and Multi-Agent Systems, 36(1), 1-31.
[6] Ruf, J., Weiss, R. J., Kropf, T., & Rosenstiel, W. (2004). Modeling and formal verification of production automation systems. In
Integration of Software Specification Techniques for Applications in Engineering (pp. 541-566). Springer, Berlin, Heidelberg.
Context
Human factors are not sufficiently considered in the design of Manufacturing Control Systems (MCS) [1]. The laboratory CRAN
proposed a meta model of social relationships of agents and employed Multi-Agent Systems (MAS) to describe future MCS [2]. The
laboratory considered the integration of humans into MCS by analysing the interaction mechanisms of agents. This work laid the
foundation for analysing the accessibility, comprehension, and adaptation between humans and systems. The technical platform
TRACILOGIS of CRAN was used to illustrate the feasibility of this formal model. However, the impacts of the proposed social
relationships on the behaviour of MCS are not adequately addressed. The laboratory would like to perform a formal verification of
MAS centred on humans, which illustrates the feasibility of the work from the theoretical aspect. The real-time properties, collision
free, safety, etc., are the major concerns of MCS [5]. Model checking is commonly used for verifying MCS [3-5]. Therefore, the goal
of this project is to be able to formally verify the above-mentioned properties of MCS centred on humans via model checking, in
order to ensure the quality of the design of MCS.
Mission
To achieve the goal of this project, the research assistant will firstly conduct the literature reviews of agent architectures and model
checking of MCS. He/She will then analyse our meta model of social relationships of agents in order to identify the most appropriate
agent architecture and model checking technique. The extension of the chosen agent architecture is potentially needed to accurately
describe the social relationships. This extension possibly necessitates the adaptation of the chosen Multi-Agent Programming
Language (MAPL). In the following, he/she will formalize the model of MCS with the updated MAPL. Next, a model transformer
will be developed to automate the verification process. Finally, a scientific paper will be demanded to conclude his/her work.
Essential requirements
Applicants are expected to have the following:
A strong background in formal verification;
Strong programming skills in Java, C++, C, etc.;
Good communication, excellent technical writing skills, and ability to prioritise work to meet deadlines;
Master degree (or equivalent) in an area pertinent to the subject area in Computer Science or a related field;
The ability to work autonomously in a multi-cultural environment.
How to apply
Applicants should send their applications to LIU Yinling (yinling.liu@univ-lorraine.fr) before 30 April 2023.
All applications must include:
A full CV;
A motivation letter;
Two recommendation letters if possible.
References
[1] El-Haouzi, H. B., & Valette, E. (2021). Human system integration as a key approach to design manufacturing control system for
Industry 4.0: Challenges, barriers, and opportunities. IFAC-PapersOnLine, 54(1), 263-268.
[2] Valette, E. (2022). Toward an anthropocentric approach for intelligent manufacturing systems' control architectures (Doctoral
dissertation, Université de Lorraine).
[3] Wooldridge, M., Fisher, M., Huget, M. P., & Parsons, S. (2002, July). Model checking multi-agent systems with MABLE. In
Proceedings of the first international joint conference on Autonomous agents and multiagent systems: part 2 (pp. 952-959).
[4] Bordini, R. H., Fisher, M., Visser, W., & Wooldridge, M. (2006). Verifying multi-agent programs by model checking. Autonomous
agents and multi-agent systems, 12(2), 239-256.
[5] Drawel, N., Bentahar, J., Laarej, A., & Rjoub, G. (2022). Formal verification of group and propagated trust in multi-agent systems.
Autonomous Agents and Multi-Agent Systems, 36(1), 1-31.
[6] Ruf, J., Weiss, R. J., Kropf, T., & Rosenstiel, W. (2004). Modeling and formal verification of production automation systems. In
Integration of Software Specification Techniques for Applications in Engineering (pp. 541-566). Springer, Berlin, Heidelberg.
Keywords:
Model checking; Multi-agent systems; Manufacturing control systems
Department(s):
| Eco-Technic systems engineering |
