Bosch Center for Artificial Intelligence

Correct-by-Construction Action Planning for Autonomous Systems


In intralogistics, a large number of mobile transport units need to be coordinated, amongst others to determine which tasks are best carried out by which unit. Along with coordination, rules and requirements have to be followed closely to ensure a safe operation of the system and a seamless interplay between the individual autonomous agents. Similar challenges arise as well in many other applications. This motivates our research in action planning for multi-agent systems, where we aim to identify optimal actions for all agents while providing a guarantee that all specifications are correctly addressed.

Traditionally, Linear Temporal Logic (LTL) provides a way to formulate goal specifications including temporal relations over a sequence of actions. This simplifies behavior design by shifting the focus away from explicitly programming execution plans to reach a certain goal. Instead, the goal itself is specified and required actions are automatically determined. Since the action sequences constructed this way are guaranteed to satisfy the specified goal, they are called correct-by-construction.

Internal view of a system with two robots in an office environment, executing the automatically generated optimal actions to achieve the following: (1) take a photo in rooms m1, m4, and m6; (2) deliver a document from desk d5 to d3; (3) guide a person at d11 to m6.

Problem and Approach

Bosch BCAI - Correct by Constructions
The team model can be constructed with size linear in the number of agents. Illustratively, this corresponds to agents passing their progress to others.

In summary, we formulate the following problem to be addressed: Given a single goal specification as LTL formula and a team of autonomous agents, automatically assign actions to these agents to optimally solve the mission while respecting all rules and constraints.

Planning the optimal actions for a complex system including many autonomously operating agents is computationally challenging. First, the state space of a multi-agent system grows exponentially in the number of agents as it reflects dependencies between the actions of different agents. Second, even when the individual tasks can be assumed to be independent, not only actions need to be planned, but also breakdown of the mission in subtasks and allocation of these to individual agents. Classically, these are considered to be two independent problems.

To address the above issues, we developed an approach called Simultaneous Task Allocation and Planning (STAP). The central aspect of STAP is to construct a team model which plans execution and considers choices for decomposing the mission and allocating tasks to different agents. Consequently, by utilizing the interplay of allocation and planning, we improve the efficiency to identify an optimal solution. In fact, utilizing the problem structure and including automated identification of decomposition choices results in a team model size of tractable complexity for increasing team sizes on the scale of tens of agents.

Bosch BCAI - Correct by Constructions
The decomposition property of a state can be seen splitting the automaton into two parts at this state. The same way as the full automaton is equivalent to the full specification, the resulting two smaller automata are equivalent to two specifications which the full specification can be decomposed.

Valid decomposition choices need to ensure two properties which need to be fulfilled by the resulting tasks. First, execution of one task must not be able to violate another task and second, completion of all tasks means completion of the overall mission given by the LTL specification. The decomposition choices can be automatically determined by translating the LTL specification into an equivalent automaton representation. In this format, the question whether and where a specification can be decomposed reduces to a property of the individual states, i.e., a state in the automaton directly corresponds to a specific decomposition choice of the LTL specification if it fulfills certain conditions.


Bosch BCAI - Correct by Construction
Even for tens of robots, the planning problem remains solvable in reasonable time. Shown is the average planning time in seconds for an increasing number of agents in an indoor transportation scenario.

In order to plan the optimal action sequence, a product is constructed between a model of the system and the automaton retrieved from the LTL specification. The resulting team model then reflects the capabilities of the system, augmented with the given specifications such that all violating actions are removed from the model and progress towards satisfaction of the goal is correctly reflected.

Optimizing the action sequence to fulfill the specification in the shortest possible time requires to minimize the maximum time required by any of the agents. However, classical single-objective planning algorithms like A* are not applicable in such a case where multiple agents are available. Consequently, a multi-objective optimization needs to be employed where the time required by each agent is considered as one objective. Additionally, incorporating knowledge about the model structure then enables to efficiently plan even for increasing numbers of agents.

To summarize, we developed a novel approach to address a critical limitation of classical task assignment problems, typically observable when planning actions for multi-agent systems: each combination of tasks needs to be planned explicitly for each of the agents in order to determine the optimal allocation. Instead, we combine planning and allocation in a single step, called Simultaneous Task Allocation and Planning (STAP).

This allows us to automatically find actions for a team of autonomous agents such that a given complex goal specification is guaranteed to be satisfied in the shortest possible time, efficiently scaling to team sizes in the tens of agents.


[1] Christel Baier and Joost-Pieter Katoen. “Principles of Model Checking”. MIT press Cambridge, 2008.

[2] Calin Belta, Boyan Yordanov, and Ebru Aydin Gol. “Formal Methods for Discrete-Time Dynamical Systems”, volume 89. Springer, 2017.

[3] Calin Belta, Antonio Bicchi, Magnus Egerstedt, Emilio Frazzoli, Eric Klavins, and George J Pappas. “Symbolic Planning and Control of Robot Motion [Grand Challenges of Robotics]”. IEEE Robotics & Automation Magazine, 14(1):61–70, 2007.

[4] Brian P Gerkey and Maja J Mataric. “A Formal Analysis and Taxonomy of Task Allocation in Multi-Robot Systems”. The International Journal of Robotics Research, 23(9):939–954, 2004.

[5] Edmund H Durfee and Shlomo Zilberstein. „Multiagent Planning, Control, and Execution”. Multiagent Systems, pages 485–545, 2013.

[6] Philipp Schillinger, Mathias Bürger, and Dimos V Dimarogonas. “Decomposition of Finite LTL Specifications for Efficient Multi-Agent Planning”. In Distributed autonomous robotic systems (DARS). Springer, 2016.

[7] Xavier Gandibleux, Frédéric Beugnies, and Sabine Randriamasy. “Martins’ Algorithm Revisited for Multi-Objective Shortest Path Problems with a MaxMin Cost Function”. 4OR, 4(1):47–59, 2006.

[8] José Manuel Paixao and José Luis Santos. “Labeling Methods for the General Case of the Multi-objective Shortest Path Problem – A Computational Study”. In Computational Intelligence and Decision Making, pages 489–502. Springer, 2013.

[9] Philipp Schillinger, Mathias Bürger, and Dimos V Dimarogonas. “Multi-Objective Search for Optimal Multi-Robot Planning with Finite LTL Specifications and Resource Constraints”. In IEEE International Conference on Robotics and Automation. Singapore, 2017.