Dissertation theses
Counterexample Guided Abstraction Refinement for Multi-robot Planning
Counterexample guided abstraction refinement (CEGAR) is a successful technique in model checking [1,2]. Within the proposed topic, the task is to investigate the possibilities of using the CEGAR technique in multi-robot planning [3,4]. Planning with many robots offers a lot of scope for designing abstractions of the problem that bring appropriate simplifications and allow the solver to solve the problem more easily, for example, some robots in the problem can be ignored, but at the cost of inaccuracies in the resulting solution. The design, search, and checking of counterexamples for a multi-robot system, with the help of which it would be possible to eliminate inaccuracies in the solution, represents another interesting challenge. Some progress has been made in multi-robot path planning, where the abstraction refinement has been made against collisions between robots. However, abstractions for path planning represent only a special case, while within this topic we would like to move the design of abstractions further towards more general multi-robot systems, where the range of robot actions is wider. An interesting direction is the extension of the CEGAR technique with abstractions that produce inaccuracy in the solution, against which the multi-robotic system is robust, and therefore there is no need to refine them.
- [1] Edmund M. Clarke, Anubhav Gupta, Ofer Strichman: SAT-based counterexample-guided abstraction refinement. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 23(7): 1113-1123 (2004)
- [2] Anubhav Gupta, Edmund M. Clarke: Reconsidering CEGAR: Learning Good Abstractions without Refinement. ICCD 2005: 591-598
- [3] Teng Guo, Si Wei Feng, Jingjin Yu: Polynomial Time Near-Time-Optimal Multi-Robot Path Planning in Three Dimensions with Applications to Large-Scale UAV Coordination. IROS 2022: 10074-10080
- [4] Lydia E. Kavraki, Steven M. LaValle: Motion Planning. Springer Handbook of Robotics, 2nd Ed. 2016: 139-162
Lazy Compilation for Classical Planning
In automated planning, the task is to find a sequence of actions that, after performing, meet a certain goal [1, 2]. This topic specifically focuses on compilation of the planning task into another formalism, such as constraint satisfaction (CSP) [3] or propositional satisfiability (SAT) [4]. Especially promising seems to be the lazy compilation, when the task is encoded into the target formalism incompletely. The encoding is subsequently refined in cooperation with the solver by generating counterexamples. The lazy compilation technique has been successfully used in the specific domain of multi-agent path finding [5]. However, the generalization of lazy compilation for classical planning is still an open question.
- [1] Malik Ghallab, Dana S. Nau, Paolo Traverso: Automated Planning and Acting. Cambridge University Press 2016, ISBN 978-1-107-03727-4
- [2] Malik Ghallab, Dana S. Nau, Paolo Traverso: Automated planning - theory and practice. Elsevier 2004, ISBN 978-1-55860-856-6, pp. I-XXVIII, 1-635
- [3] Rina Dechter: Constraint processing. Elsevier Morgan Kaufmann 2003, ISBN 978-1-55860-890-0
- [4] Armin Biere, Marijn Heule, Hans van Maaren, Toby Walsh: Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications 185, IOS Press 2009, ISBN 978-1-58603-929-5
- [5] Pavel Surynek: Unifying Search-based and Compilation-based Approaches to Multi-agent Path Finding through Satisfiability Modulo Theories. Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI 2019), pp. 1916-1922, Macau, China, International Joint Conferences on Artificial Intelligence, 2019, ISBN (Online): 978-0-9992411-4-1
Motion Planning for Multi-Robot Systems with Many Degrees of Freedom
Thanks to algorithmic techniques such as continuous conflict-based search (CCBS), it has become possible to plan the movement of large groups of relatively simple robots with a small number of degrees of freedom for movement, which is especially useful in warehouse logistics. For more complex robots with more degrees of freedom, current techniques rely on planning movement in joint configuration spaces, the complexity of which increases exponentially with the increasing number of robots and the number of their degrees of freedom for movement. These techniques therefore prove to be inefficient for real-world use, which is why we practically do not encounter multi-robot systems consisting of more complex robots.
In this topic, we would like to explore alternative methods of motion planning for multi-robot systems that do not work with a joint configuration space and, similarly to multi-agent pathfinding (MAPF) techniques, deal only with the conflicts (spatial collisions) that arise between robots. It is possible to focus on a specific type of robot that is characterized by many degrees of freedom, for example, 6-axis or 7-axis robotic arms (in which case the research can be extended to experiments with real robots in the Robotic Agent Laboratory - RoboAgeLab). In terms of conflict elimination techniques, the research can be based on conflict-based search (CBS), or it can be based on compilation approaches that translate the problem into another formalism, such as propositional satisfiability (SAT) or constraint satisfaction (CSP), or it is possible to combine compilation techniques with counterexample guided abstraction refinement (CEGAR).
Multi-agent Path Finding in Continuous Spaces
Specialist supervisor: doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Multi-agent path finding (MAPF) is the problem of computing collision-free paths from given starting positions to goal positions for a set of agents [1,2]. The MAPF problem is motivated by a number of real-world applications, for example agents can model robots for transporting goods in warehouses. Traditional solutions to this problem are based on models where both time and space are discrete. However, continuous models would be more realistic. The current state-of-the-art in this topic allows agents to move continuously along linear trajectories [3,4]. The goal of this work is to contribute to more general techniques, for example to allow agents to move along non-linear trajectories, or to model certain kinematic properties of agents, such as acceleration, or other properties that manifest themselves in a continuous model of the problem.
- [1] David Silver: Cooperative Pathfinding. AIIDE 2005: 117-122
- [2] Ko-Hsin Cindy Wang, Adi Botea: MAPP: a Scalable Multi-Agent Path Planning Algorithm with Tractability and Completeness Guarantees. J. Artif. Intell. Res. 42: 55-90 (2011)
- [3] Thayne T. Walker, Nathan R. Sturtevant, Ariel Felner: Extended Increasing Cost Tree Search for Non-Unit Cost Domains. IJCAI 2018: 534-540
- [4] Anton Andreychuk, Konstantin S. Yakovlev, Pavel Surynek, Dor Atzmon, Roni Stern: Multi-agent pathfinding with continuous time. Artif. Intell. 305: 103662 (2022)