Supervisors

Suitable for

Abstract

Reactive synthesis represents the culmination of declarative programming. By focusing on what a system should accomplish rather than how to achieve it we are able, on the one hand, to simplify the system design process while avoiding human mistakes and, on the other hand, to allow an autonomous agent to self-program itself just from high-level specifications. Linear Temporal Logic (LTL) or LTL on finite traces (LTLf) synthesis is one of the most popular variants of reactive synthesis, being the problem of automatically designing correct-by-construction reactive systems with the guarantee that all its behaviours comply with desired dynamic properties expressed in LTL/LTLf.

Recently, there has been a growing interest in applying Large Language Models (LLMs) to various problems in computer science such as Automated Reasoning, Knowledge Representations and Planning, and Formal Methods in general. Emerging studies have explored the capabilities of LLMs in these fields.

The objective of this project is to investigate the feasibility and effectiveness of using LLMs for reactive synthesis problems with specifications expressed in LTL and LTLf.

Focus:

• Insights into the potential and limitations of LLMs for reactive synthesis with LTL and LTLf specifications.

• An LLM-guided reactive synthesis framework that integrates natural language processing into the synthesis process.

• Empirical evaluation of the performance and effectiveness of LLM-based synthesis algorithms.

References:

• Amir Pnueli The Temporal Logic of Programs. FOCS 1977: 46-57

• Amir Pnueli, Roni Rosner: On the Synthesis of a Reactive Module. POPL 1989: 179-190

• Giuseppe De Giacomo, Moshe Y. Vardi: Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. IJCAI 2013: 854-860

• Giuseppe De Giacomo , Moshe Y. Vardi: Synthesis for LTL and LDL on Finite Traces. IJCAI • Philipp J. Meyer, Salomon Sickert, Michael Luttenberger: Strix: Explicit Reactive Synthesis Strikes Back! CAV (1) 2018: 578-586 • Marco Favorito, Shufang Zhu. LydiaSyft: A Compositional Symbolic Synthesizer for LTLf Specifications

• Karthik Valmeekam, Matthew Marquez, Sarath Sreedharan, Subbarao Kambhampati: On the Planning Abilities of Large Language Models - A Critical Investigation. CoRR abs/2305.15771 (2023)

Pre-requisites: Foundations of Self-Programming Agents and Computer-Aided Formal Verification not required but will help