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

AI summary

Overview

Research area: Robotics — probabilistic planning under uncertainty, human-robot interaction, and the intersection of large language models with formal methods (logic programming and model checking).

Technical level: Intermediate. Readers need basic familiarity with Markov Decision Processes, logic programming (Prolog), and formal verification concepts, but the paper is written for a robotics audience rather than a pure formal-methods audience.

Scope: The paper presents and empirically evaluates an open-source framework that turns a natural-language description of a robotic scenario into a Prolog knowledge base, an MDP, and an executable optimal policy, validated on three domains (structure building, AGVs in a factory, and the gripper domain).

What This Paper Is About

Robots operating around humans need policies that handle uncertainty, and Markov Decision Processes are a standard way to model and solve such problems. The bottleneck is that building an MDP normally requires someone to write down a complete symbolic domain specification by hand, even though the knowledge about the scenario usually exists only as informal human language. This paper's goal is to derive optimal policies directly from a natural-language scenario description, using an LLM to generate the formal knowledge base and off-the-shelf tools to do the MDP construction and policy synthesis.

Key Contributions

1. An open-source framework (https://www.github.com/idra-lab/prolog_mdp) that takes a natural-language narrative as input, uses few-shot prompting with an LLM (GPT-4o or GPT-5-mini) to generate a Prolog knowledge base, and converts that KB into a PRISM-format MDP.

2. An automated MDP generator implemented in Prolog that performs reachability analysis from the initial state, then refines transition probabilities, assigns rewards, and compiles an MDP graph into a PRISM script — no manual MDP authoring required.

3. A reward specification scheme that distinguishes necessary conditions (hard constraints; a single violation assigns a fixed large negative penalty and stops further evaluation) from sufficient conditions (desirable properties that accumulate non-negative values). The LLM decides this necessary/sufficient classification itself during reward generation.

4. An end-to-end pipeline that exports the policy synthesized by the Storm model checker as a state-action table, which the authors executed in a ROS2 workspace for a real-world robotic experiment.

Main Findings

• KB generation generalises across domains. GPT-4o produced a correct KB in all five structure-building tests and all five AGV tests, and in three of five gripper tests without any new examples. The remaining GPT-4o errors were reported as syntax-level mistakes, not conceptual ones.

• Small, easily correctable errors. In gripper cases 4 and 5, GPT-4o used ball3 instead of ball3_position. In AGV scenario 4, it added a non-instantiated predicate to the verify predicate list, which the SWI-Prolog interpreter flagged immediately. All reported errors were correctable by an expert, with the noted count X(2,2) for gripper case 4 and X(1,1) for gripper case 5 (N logical errors, M corrections).

• A stronger model achieved a perfect score. On additional tests, GPT-5-mini generated a correct KB in all fifteen reported cases.

• Runtime depends heavily on MDP size and on the number of actions per state. State counts ranged from 17 to 1024 in structure building, 35 to 194 in AGV, and 14 to 2027 in grippers. The AGV cases (2 or 3 actions) were solved consistently faster than structure building (16, 27 or 28 actions). The paper states that the probability-refinement step's cost grows with the number of available actions per state and often dominates total computation time.

• Large MDPs are expensive. The structure-building case with 1024 states and 27 actions took 28.928 s for MDP generation, 780.792 s for probability refinement, and 374.034 s for writing to file. The gripper case with 2027 states and 18 actions took 3.184 s, 0.999 s, and 0.298 s respectively.

• Policies respect the stated objectives. The extracted policies satisfied the criteria written in the input queries, both when maximising the probability of success and when minimising reward, in every domain.

• Not yet an online tool. The authors explicitly state that the negligible KB and MDP generation times observed on these examples "does not mean that the framework could be used for online generation in industrial scale applications."

• Two optimisation labels are generated. The LLM produces doneP (maximise probability of success) and doneR (minimise reward). The user chooses which to use, because the optimal final state can differ between them — for example, in the AGV case doneP requires reaching the final section without emergency stops while doneR prioritises speed regardless of stops.

• Human validation is retained by design. A human operator checks and, if needed, fixes the generated KB; the framework is presented as augmenting rather than replacing domain experts and system designers.

Methodology in Plain English

The authors split the problem into an LLM front end and a formal back end.

Front end (KB generation). A domain expert writes a plain-text description of the scenario, which is passed to an LLM together with curated few-shot examples. Some examples are general — they show how an action must be structured (name and arguments, preconditions, effects), how the initial state must be formatted, and which labels Storm should receive. Others are use-case specific: one example shows KB generation, a second shows actions, a third shows rewards, and each includes counterexamples illustrating wrong modelling choices. The LLM must wrap its output in Markdown-like tags (kb, action, reward) so a Python parser can extract the parts.

The KB is generated incrementally rather than in one pass: the model first produces the initial state, that output is fed back in with the original query to generate the actions, and both are fed back again to generate the rewards. The authors state this incremental approach produced more accurate and coherent outputs than single-pass generation in preliminary experiments. The resulting Prolog KB stores the initial state, immutable grounded predicates, actions, reward functions, and auxiliary functions that write the MDP in PRISM formalism. Reward functions are pure Prolog code written by the LLM, split into necessary and sufficient conditions.

Back end (MDP generation), in four steps. (1) Graph generation: starting from the initial state, the algorithm recursively checks whether each action's preconditions hold; if so it applies the probabilistic effects and grounds lifted predicates exhaustively, producing new states — a full reachability analysis. If a delete effect cannot be grounded, the algorithm adds a self-transition (a no-op) rather than blocking the action. (2) Probability refinement: probabilities attached to an action's effect sets do not depend on how many states that action generates, so the framework traverses the graph and, for edges sharing the same source state, action, and effect set but leading to different states, splits the probability across them — uniformly in the illustration given (0.9 becomes 0.45 and 0.45). (3) Reward generation: necessary conditions are checked first; any violation assigns a fixed large negative penalty and halts evaluation. If all pass, sufficient conditions contribute non-negative values that accumulate. (4) PRISM script compilation: the header is built from LLM-generated variable-initialisation strings, the transition model is written by traversing the graph, and the labels are emitted, producing a file ready for Storm.

Policy synthesis and execution. Storm is queried with a property such as Pmax=? [ F "doneP" ] or Rmin=? [ F "doneR" ] through the stormpy Python wrapper. The resulting policy is exported as a state-action table for use in a robotic runtime such as ROS2.

Experiment setup. Five tests were run per use case. Experiments ran on Ubuntu 22.04 with an AMD Ryzen 7 7700X CPU and 64GB of DDR5 memory, using SWI-Prolog version 9.2.9 and stormpy version 1.9.0. GPT-4o and GPT-5-mini were used with temperature set to 0 and a fixed seed of 42; the authors note this does not produce repeatable behaviour but reduces LLM unpredictability. Table I results are averaged over 100 trials, and policy-extraction times are averaged over 10000 runs. Data collection and experiments were conducted under ethics committee approval at the University of Trento, application No. 2025-003.

The three use cases. Structure building: a human selects blocks from a tray placed by a robotic manipulator and builds towers, with the reward encouraging diversity of available blocks (freedom of choice) and a necessary constraint that no two pillars differ in height by more than one block. AGV traffic management: an autonomous guided vehicle crosses factory sections containing workers; the wait action avoids collisions but adds delay, while proceed risks an emergency stop. Gripper domain: a two-gripper robot moves balls between rooms with probabilistic pick and drop actions, including variants with energy limits and high-value ball prioritisation.

Why This Matters

The paper targets a practical bottleneck: probabilistic models are powerful but expensive to author, and the knowledge needed to author them typically lives in prose, not in formal specifications. By automating the translation while keeping the intermediate representation human-readable and inspectable, the framework aims to make probabilistic planning more accessible and more trustworthy in safety-relevant robotics.

Impact on research. It offers a concrete data point on combining LLMs with formal methods rather than using LLMs as standalone planners — the LLM handles language-to-symbol translation and reward structuring, while reachability analysis, probability distribution, and policy optimisation are handled by deterministic tools. The reported generalisation to unseen action types (such as the architrave action and the speed-up action) and to configurations outside the few-shot examples is the paper's central empirical claim.

Real-world applications:

• Collaborative manufacturing, where a robot arm places materials and a human worker chooses among them, with the policy encouraging human freedom of choice while enforcing safety constraints.
• Factory logistics with autonomous guided vehicles sharing floor space with workers, where the trade-off between throughput (low delay) and safety (avoiding emergency stops) is explicit in the reward design.
• Warehouse or laboratory pick-and-place with grippers, where pick and drop actions fail probabilistically and energy or value constraints matter.
• Any deployment where an expert can describe a routine in words but cannot write a PPDDL or RDDL model — the paper explicitly frames the LLM-plus-KB approach as a response to the limited expressiveness of those languages.

Industry relevance. The authors state that the resulting MDPs "yield effective policies suitable for industrial applications" and demonstrate real execution through a ROS2 workspace. However, they also caution that the current generation times do not support online generation at industrial scale, which frames the framework as an offline design-time tool for now.

Future Directions

• Automatic error detection and repair. The observed LLM mistakes were syntax-level, and the authors suggest integrating syntax and consistency-checking tools so that errors like ball3 versus ball3_position are caught without expert intervention.

• Scaling to online or industrial-scale generation. Total time is dominated by probability refinement and file writing for large MDPs, and the paper explicitly declines to claim online capability. Reducing this cost is the obvious next step.

• Broader and less example-dependent generalisation. The gripper domain was tested without new examples and produced the most errors with GPT-4o, so whether few-shot prompting, fine-tuning, or stronger models can remove the need for curated examples remains open.

• Extending beyond the tested settings. Only the structure-building use case had a real-world experiment; the AGV and gripper cases were validated purely in simulation because the authors lacked access to the necessary hardware and resources.

• Verifying policy execution quality. Table II reports simulation results of policy execution, but the provided paper content is truncated at that table, so the specific execution figures are not reported here.

Target Audience

Robotics and AI researchers working on planning under uncertainty, human-robot interaction, or neuro-symbolic methods; formal-methods researchers interested in LLM-assisted model construction; and applied engineers who need probabilistic policies for collaborative or mobile robot deployments but lack the resources to hand-author MDP models. Practitioners evaluating whether LLM-generated formal artifacts are reliable enough for safety-relevant robotics will find the error analysis and the runtime measurements particularly useful.

Authors’ 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.