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
Requirement of the thesis
Contact Rong Gu (rong.gu@mdu.se) |
Start date: | |
End date: | |
Prerequisites: |
|
IDT supervisors: | Rong Gu |
Examiner: | Cristina Seceleanu |
Comments: | |
Company contact: |