Automated Generation of MDPs Using Logic Programming and LLMs for Robotic Applications
Enrico Saccon, Davide De Martini, Matteo Saveriano, Edoardo Lamon, Luigi Palopoli, Marco Roveri
AI summary
Problem
Creating Markov Decision Processes for robotic planning typically requires complex symbolic specifications that are difficult to derive from informal human descriptions, limiting scalability and accessibility.
Approach
The framework uses an LLM to extract structured Prolog knowledge bases from natural language, automatically constructs the corresponding MDP through reachability analysis, and synthesizes optimal policies using a formal model checker.
Key results
- Automated conversion of natural language to Prolog knowledge bases via few-shot prompting
- Automatic MDP construction and reachability analysis from logical predicates
- Synthesis of optimal probabilistic policies using the Storm model checker
- Successful validation across three human-robot interaction scenarios with minimal manual effort
Why it matters
Provides a scalable, interpretable pipeline for deploying reliable probabilistic planning in real-world robotic applications involving human interaction.
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 poli- cies 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 formalmethodstoenablemoreaccessibleandscalableprobabilistic planning in robotics.