Till Hofmann: Towards Bridging the Gap between High-Level Reasoning and Execution on Robots



Till Hofmann

Ehem. assoziierter Promotionsstudent


+49 241 80-21639



Formalisms such as Golog […] and PDDL […] allow the specification of a robot’s behavior in an abstract manner. Based on a logical model of the environment, the agent’s actions are specified with preconditions and effects. This allows for determining the course of action by searching for an appropriate action sequence (PDDL), possibly intertwined with agent programs specified by the user (Golog). However, when deploying such a system on a real robot, one often faces additional challenges, such as the need to calibrate a robot arm before its usage. Those issues are intentionally ignored when specifying the abstract behavior, as it would impair the reasoner performance. This research project aims to close the gap between high-level reasoning and low-level robot platform [Hofmann et al., 2018]. Instead of specifying all the low-level details in the reasoning domain, we instead model the platform components separately as timed automata. Then, we specify constraints that connect a high-level program with the platform, e.g., by requiring that the arm needs to be calibrated five seconds before the robot picks up an object. We then need to transform the high-level program into a sequence of actions that satisfies all those constraints, resulting in a task specification that follows the high-level program while dealing with the low-level platform details.

A logic for specifying metric temporal constraints for Golog programs
In the first step, we extended ESG, a modal variant of the Situation Calculus that allows temporal constraints, with metric temporal constraints [Hofmann & Lakemeyer, 2018]. The resulting logic retains most of the properties of ESG and thus allows the specification of basic action theories and Golog programs extended with metric constraints.

Plan Transformation based on Timed Automata Reachability Analysis
In a first approach to solve the temporal platform constraints, we have looked at timed automata reachability analysis [Viehmann, Hofmann, Lakemeyer, 2021]. In a first step, we transform a high-level action sequence into a timed automaton such that each action is one location in the resulting automaton. This automaton is then combined with the platform model such that in the product automaton, all edges that violate a constraint are removed. Finally, we apply reachability analysis using the model checking tool UPPAAL [Behrmann et al., 2004]. The resulting path describes the transitions of the platform models such that all constraints are satisfied during the execution of the original plan. Despite the combinatorial blowup due to the automata product, this approach performs well and we were able to transform plans with 50 actions and several platform components in a few seconds.

Controller Synthesis for Golog Programs
However, the first approach poses some limitations: For one, it only works on pre-determined plans. Thus, it cannot be used with any formalism that uses online sensing, as this would require online decision making. Also, it does not distinguish between controllable actions (e.g., starting to pick up an object) and actions that are controlled by the environment (e.g., the arm going into an error state, or even the end of an action). To tackle those limitations, we used a different approach based on MTL synthesis. Instead of applying reachability analysis, we build on top of results on controller synthesis for MTL specifications [Bouyer et al., 2006]. We first convert a given Golog program into a timed automaton, apply MTL controller synthesis on the automaton, the platform model, and the platform constraints, and then use the resulting controller to guide the Golog executor. We have presented the theory of the approach in [Hofmann & Lakemeyer, 2020] and we have been working on an implementation in cooperation with the former UnRAVeL researcher Stefan Schupp [Hofmann & Schupp, 2021; Hofmann & Schupp, 2022].

Explanatory diagnosis to recover from faults
Apart from dealing with platform constraints, executing a high-level plan on a mobile robot also needs to deal with faults that occur during execution. Based on the same platform models that we used for plan transformation, we can apply diagnosis to analyze and recover from an error. In history-based diagnosis, we provide possible (faulty) alternatives to the actions in a plan that have different, undesired effects. Based on the sensed observations, we then determine the plan variant that actually occurred. Previously, this was done by directly modifying the plan. We have shown that if we use an automata-based model of the platform and exogenous actions that change the state of a platform component, we can obtain better explanations and, even more importantly, determine a recovery plan that can revert the fault [Habering, Hofmann, Lakemeyer, 2021].


Behrmann, G., David, A., & Larsen, K. G. (2004). A Tutorial on Uppaal. In M. Bernardo & F. Corradini (Eds.), Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, Bertinora, Italy, September 13-18, 2004, Revised Lectures (pp. 200–236). Springer.

Bouyer, P., Bozzelli, L., & Chevalier, F. (2006). Controller Synthesis for MTL Specifications. In C. Baier & H. Hermanns (Eds.), Proceedings of the 17th International Conference on Concurrency Theory (CONCUR) (pp. 450–464). Springer Berlin Heidelberg.

Habering, D., Hofmann, T. & Lakemeyer, G. (2021). Using platform models for a guided explanatory diagnosis generation for mobile robots. in Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI) 1908–1914.

Hofmann, T., & Lakemeyer, G. (2018). A logic for specifying metric temporal constraints for Golog programs. Proceedings of the 11th Cognitive Robotics Workshop 2018 (CogRob).

Hofmann, T., Mataré, V., Schiffer, S., Ferrein, A., & Lakemeyer, G. (2018). Constraint-based online transformation of abstract plans into executable robot actions. AAAI Spring Symposium: Integrating Representation, Reasoning, Learning, and Execution for Goal Directed Autonomy.

Hofmann, T. & Schupp, S (2021). TACoS: A tool for MTL controller synthesis. in Proceedings of the 19th International Conference on Software Engineering and Formal Methods (SEFM) 372–379. Springer.

Hofmann, T. & Schupp, S. (2022). Controlling Timed Automata against MTL Specifications with TACoS. Science of Computer Programming. Elsevier. to appear.

Levesque, H. J., Reiter, R., Lesperance, Y., Lin, F., & Scherl, R. B. (1997). GOLOG: a logic programming language for dynamic domains. Journal of Logic Programming, 31(1–3).

McDermott, D., Ghallab, M., Howe, A., Knoblock, C., Ram, A., Veloso, M., Weld, D., & Wilkins, D. (1998). PDDL - The Planning Domain Definition Language. The AIPS-98 Planning Competition Committee.

Viehmann, T., Hofmann, T. & Lakemeyer, G. (2021). Transforming robotic plans with timed automata to solve temporal platform constraints. in Proceedings of the 30th International Joint Conference on Artificial Intelligence (IJCAI) 2083–2089.