Automated Generation of MDPs Using Logic Programming and LLMs for Robotic Applications

TL;DR

The paper presents an open-source framework that converts informal natural language robot-domain descriptions into executable probabilistic policies. It leverages LLMs to build a Prolog knowledge base, derives an MDP via reachability analysis, and uses the Storm model checker to synthesize optimal policies, which are exported for ROS2 execution. Across three use-cases, the approach demonstrates generalisation, robustness, and practical deployment, while highlighting the need for improved reliability and automation in handling LLM-generated outputs. This work advances accessible, formal, and scalable probabilistic planning for human-robot interaction in uncertain environments.

Abstract

We present a novel framework that integrates Large Language Models (LLMs) with automated planning and formal verification to streamline the creation and use of Markov Decision Processes (MDP). Our system leverages LLMs to extract structured knowledge in the form of a Prolog knowledge base from natural language (NL) descriptions. It then automatically constructs an MDP through reachability analysis, and synthesises optimal policies using the Storm model checker. The resulting policy is exported as a state-action table for execution. We validate the framework in three human-robot interaction scenarios, demonstrating its ability to produce executable policies with minimal manual effort. This work highlights the potential of combining language models with formal methods to enable more accessible and scalable probabilistic planning in robotics.

Figures (11)

• Figure 1: General diagram of the framework. Given an NL description of the query, it generates a Prolog KB through few-shot prompting with an LLM. The KB is used to extract a PRISM MDP, which Storm uses to synthesize an optima policy. The policy can then be used to execute actions.
• Figure 2: An example of an auxiliary function to generate the PRISM variables: there are three pillars, P1, P2, and P3, which are integers and can have a value between 0 and 4, plus the reward value which is defined as an integer.
• Figure 3: Example of a query passed as input to the LLM to generate the MDP.
• Figure 4: An example of how the output from the LLM should be formatted.
• Figure 5: An answer used as example for the LLM, containing how to generate the KB from the query shown in Fig. \ref{['fig:query_ex']}.