Symbolic Linear Temporal Logic over Finite Traces Synthesis - Moshe Vardi

Moshe Vardi, Professor at Rice University and one of the most influential figures in logic, verification, and theoretical computer science, discusses his paper “Symbolic LTLf Synthesis”.

This conversation explores how Linear Temporal Logic over finite traces (LTLf) provides a more practical and scalable foundation for program and controller synthesis, especially compared to classical approaches based on infinite executions. The discussion traces the deep theoretical roots of synthesis in logic, automata, and games, while connecting them to modern challenges in AI, planning, and autonomy.

Moshe shares the origin story of the paper, which grew out of collaborations with AI researchers and a visiting student, explains why “simpler” finite-trace reasoning turned out to be a strength rather than a limitation, and reflects on how LTLf has helped shift the direction of research and tooling in temporal synthesis.

In This Episode -

• The history of program synthesis

• Why infinite traces dominate classical LTL

• Linear Temporal Logic over finite traces (LTLf)

• Automata theory in both verification and synthesis

• Implications for reactive systems, autonomy, and agent design

• The future of symbolic synthesis + neurosymbolic AI research

About the Paper -

“Symbolic LTLf Synthesis”

Shufang Zhu, Lucas M. Tabajara, Jianwen Li, Geguang Pu, Moshe Y. Vardi

IJCAI, 2017

This paper introduces an automata-based approach to synthesizing controllers from LTLf specifications, leveraging the finite-trace setting to achieve simpler constructions and improved scalability. It demonstrates how symbolic techniques can make temporal synthesis more practical for AI and planning-oriented applications.

https://arxiv.org/abs/1705.08426

About the Guest -

Moshe Vardi is University Professor at Rice University, where his research spans logic, automata theory, formal verification, and the foundations of computer science. He has played a central role in bringing temporal logic and model checking from theory into industrial practice, while also contributing to broader discussions about AI and society.

https://www.cs.rice.edu/~vardi/

Credits -

• Host & Music: Bryan Landers, Technical Staff, Ndea

• Co-Host: Mark Santolucito, Assistant Professor, Barnard College/Columbia U

• Editor: Alejandro Ramirez

• https://x.com/ndea

• https://x.com/bryanlanders

• https://ndea.com