Research map / Learning theory and algorithms / Combinatorial and search optimization
Adaptive Reactive Synthesis for LTL and LTLf Modulo Theories
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Proposes the first reactive synthesis procedure for LTL modulo theories (LTLT) and LTLf modulo theories, combining a Booleanized controller with an on-the-fly SMT-based provider that produces theory outputs and supports adaptive (soft-constraint) responses.
Problem
Reactive synthesis for LTL and LTLf specifications whose atomic propositions are literals from first-order theories, where the system must output theory-valued variables at each step; prior work only handled realizability via Boolean abstraction, with no full synthesis procedure.
Approach
Synthesize a static Boolean controller from the Booleanized LTL specification, then at runtime use a partitioner to discretize environment inputs, the Boolean controller to choose a literal valuation, and an SMT solver to produce concrete theory outputs satisfying the chosen existential formula; soft constraints added to the SMT query enable adaptive responses without re-synthesis.
Key results
- All input-output steps in the experiments took under 1 ms per timestep; the Boolean controller averaged about 2 microseconds and the provider about 170 microseconds.
- Compared with Wu et al. 2019 on the same tasks, the approach needed about 0.2 µs for the Boolean output versus 0.5 µs for theirs, and about 0.17 ms versus 0.5 ms for the theory output.
- Adaptive soft constraints (min/max, closest-to-point, smoothness) changed provider outputs without re-synthesizing the controller, with comparable provider times.
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use a Boolean controller for the Boolean output task | On-the-fly synthesis vs. Wu et al. (2019) · Table 3 tasks | Boolean output time (µs): 0.5µs vs 0.2µs | Helped |
| Use on-the-fly synthesis for final value production | On-the-fly synthesis vs. Wu et al. (2019) · Table 3 tasks | Final value production time (µs): 0.17ms vs 0.5ms | Helped |
| Add smoothness adaptivity | On-the-fly synthesis · Pw. All | Final value production time (µs): 214 -> 205 | Helped |
| Add moving-p adaptivity | On-the-fly synthesis · Pw. All | Final value production time (µs): 214 -> 215 | Hurt |
| Add smoothness adaptivity | On-the-fly synthesis · Driv. 1, , 2 | Final value production time (µs): 124 -> 123 | Helped |
| Add moving-p adaptivity | On-the-fly synthesis · Driv. 1, , 2 | Final value production time (µs): 124 -> 130 | Hurt |
| Add smoothness adaptivity | On-the-fly synthesis · Cr. All | Final value production time (µs): 133 -> 138 | Hurt |
| Add moving-p adaptivity | On-the-fly synthesis · Cr. All | Final value production time (µs): 133 -> 101 | Helped |
Surprising findings
- Some adaptive (MaxSMT-style) queries ran faster than the plain solve queries, attributed to Z3's optimize() behaving more regularly in some cases.
Limitations
- Termination is not guaranteed for semi-decidable theories; the approach yields only partial solutions there.
- Requires the theory to admit an efficient procedure for models of existential fragments and decidability in the exists-forall fragment for Booleanization.
- Experiments are limited to a prototype in Python with Z3 and Strix on small benchmarks.
Experimental setup
Datasets: Cooker Usb Lift Train Connect Stage Synthetic (Syn.) scalability benchmarks
Benchmarks: Cooker Usb Lift Train Connect Stage Synthetic scalability benchmarks
Metrics: partitioner time Boolean controller time provider time Boolean abstraction time controller synthesis time
Baselines: Wu et al. 2019 shield-based approach
Builds on: Boolean abstraction for LTL modulo theories (Rodriguez and Sánchez 2023) Strix Z3
Closest papers by meaning
- Foundations of Reactive Synthesis for Declarative Process Specifications (AAAI 2024 · similarity 0.89)
- LTLf Synthesis Under Unreliable Input (AAAI 2025 · similarity 0.88)
- Shield Synthesis for LTL Modulo Theories (AAAI 2025 · similarity 0.86)
- DeepLTL: Learning to Efficiently Satisfy Complex LTL Specifications for Multi-Task RL (ICLR 2025 · similarity 0.85)
- LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments (AAAI 2025 · similarity 0.85)
- Situation Calculus Temporally Lifted Abstractions for Generalized Planning (AAAI 2025 · similarity 0.84)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.