Bachelor and Master Theses

To apply for conducting this thesis, please contact the thesis supervisor(s).
Title: Towards a Platform of Model Checked Multi-Agent Planning
Subject: Computer science
Level: Advanced
Description:

Overall Description

Agents are systems that can move, function, and collaborate with others (e.g., humans or machines) without human intervention. Self-driving cars, drones, robots, and autonomous construction equipment are examples of agents in our real lives.

Agents are often designed to accomplish missions in a group, such as robots delivering goods in a warehouse, and wheel loaders digging and transporting stones in a quarry. To accomplish their missions, they need to collaborate and cooperate with each other. For example, in Fig.1, a small group of robots (i.e., blue ones) is assigned to a specific region of an area (e.g., a warehouse) and responsible for collecting goods within that region and transporting them to a port that connects the region to another. The other group of robots (i.e., yellow ones) is responsible for collecting the goods from the port and keep carrying them to the destination.

Fig 1. An example of multi-agent systems

Multi-agent planning (MAP) is about planning actions in an optimal manner so that they can accomplish their missions in an efficient way. In the example shown in Fig.1, MAP is about planning the robots' movement and order of picking up goods at different points so that all the goods can be delivered to the destination in the fastest way.

For planning, machine learning is a popular way of training agents to behave in a certain manner s.t. they accomplish their missions in time. Methods such as Q learning, deep learning, and Monte-Carlo tree search, are been used in solving the MAP problems.

Besides planning itself, safety is another important factor that one needs to consider in MAP. Free of collision is one typical safety requirement. Never being stuck in a starving situation is another example of a safety requirement, which means that robots should never be waiting for each other s.t. a deadlock of waiting happens. Guarantee that MAP satisfies the safety requirement is a difficult problem but as important as planning itself because agents are often safety critical. A minor error may cause a catastrophic consequence. Formal methods, e.g., model checking, are techniques that are based on mathematics. They provide a way of proving that the target system is free of bugs in the sense that the system satisfies its requirements.

So far, there is no such platform in academia nor in industries that provides an integrated way of simulation, training, learning, and verification of MAP. In this thesis, you will be conducting research toward a platform for model-checked multi-agent planning.

Content of the thesis

  • Read the latest literature on MAP and understand the frontier of this field.
  • Analyze classic MAP problems and propose a meta-model for building agent models and environment models. Tools for modeling: UPPAAL5 and OpenAI Gym.
  • Verify the resulting plans in UPPAAL STRATEGO against safety requirements.
  • Conduct agent training in Open AI Gym.
  • Demonstrate the generosity and applicability of the meta-models by solving one or two classic MAP problems. Comparing the performance of your method to the state-of-the-art methods.

Requirement of the thesis

  • Discrete mathematics.
  • Capability of reading scientific literature.
  • Knowledge of modeling. The modeling language is not required. For example, modeling in Matlab, Simulink, and UML tools.
  • Some knowledge of reinforcement learning/machine learning.

Contact

Rong Gu (rong.gu@mdu.se)

Start date:
End date:
Prerequisites:
  • Discrete mathematics.
  • Capability of reading scientific literature.
  • Knowledge of modeling. For example, modeling in Matlab, Simulink, and UML tools.
  • Some knowledge of reinforcement learning/machine learning.
IDT supervisors: Rong Gu
Examiner: Cristina Seceleanu
Comments:
Company contact: