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.