NAISS
SUPR
NAISS Projects
SUPR
LTL2PDDL: Symbolic Reactive Synthesis on Planning Domains
Dnr:

NAISS 2026/4-1531

Type:

NAISS Small

Principal Investigator:

Taiquan Sui

Affiliation:

Chalmers tekniska högskola

Start Date:

2026-09-06

End Date:

2027-04-01

Primary Classification:

10201: Computer Sciences

Webpage:

Allocation

Abstract

Reactive synthesis is an approach for automatically constructing reactive systems from high-level descriptions of desired behaviour. Linear Temporal Logic (LTL) is commonly used to specify such behaviours, but encoding complex environments entirely in LTL can lead to cumbersome and inefficient models. This project investigates a symbolic and compositional approach to reactive synthesis over planning domains. The central idea is to combine Planning Domain Definition Language (PDDL) descriptions of complex environments with temporal objectives expressed in LTL. PDDL is used to describe the structure and dynamics of the underlying domain, while LTL specifies the desired behaviour over time. The project develops new synthesis infrastructure for symbolically represented game arenas and expressive winning conditions. It also investigates suitable fragments of PDDL, translations between planning and synthesis representations, and abstraction-refinement techniques for scalable game solving. The aim is to exploit the structural and symbolic information present in planning domains to handle substantially richer synthesis problems than those that can conveniently be represented directly in LTL. The developed methods will be evaluated experimentally on benchmark families of increasing complexity, with particular emphasis on scalability and comparison of alternative synthesis and solving techniques.