Model-Guided Synthesis for LTL over Finite Traces
summary
MoGuS repeatedly invokes an LTLf satisfiability checker to get concrete satisfying traces, uses formula-progression to generate TDFA states on the fly, and marks states that can never lead to a winning strategy as failure states, rolling back until the initial state is classified MoGuS returns Realizable or Unrealizable. The approach often avoids constructing the full double‑exponential deterministic automaton, and on a large benchmark suite it shows the most stable and best overall performance, outperforming prior top‑down and bottom‑up tools on many large formulas.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 0:21LTL over finite traces
- 2:10Reactive synthesis problem
- 3:57LTLf synthesis to DFA games
- 5:45Top-down vs bottom-up synthesis
- 7:14Model-guided synthesis with MOGUS
- 8:44MOGUS performance gains
- 10:33Experimental results
- 12:22Conclusion
- 13:46Q&A
related talks
21mVerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model,(…)
01h 04mInvited Talk: Finding Good Programs by Avoiding Bad Ones
24mReward-Guided Synthesis of Intelligent Agents with Control Structures
15mToward Neural-Network-Guided Program Synthesis and Verification
53mSemantics-based program manipulation in the age of LLMs
21mTowards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
19mAutomated Program Refinement: Guide and Verify Code Large Language Model with(…)
34mMaking state management intelligent