让下一篇重要论文，不再错过。

原文摘要

Linear Temporal Logic (LTL) provides a rigorous framework for specifying long-horizon robotic tasks, yet existing approaches face a trade-off: model-based synthesis relies on accurate labeled transition systems, whereas learning-based methods often require online interaction, task-specific rewards, or specification-conditioned training. We study LTL-specified robotic planning and execution in an offline, model-free setting, where the agent is given only fixed, task-agnostic trajectory fragments, with no dynamics model, task demonstrations, or online data collection. To address this setting, we propose SAGAS, a framework that combines the compositionality of symbolic synthesis with the data-driven reachability structure learned from offline trajectories. SAGAS first learns a reusable latent reachability graph and a frozen goal-conditioned executor from fragmented offline data. For each new LTL formula, it performs task-time semantic graph augmentation to ground state-defined propositions on the learned graph and applies Büchi product search to synthesize a cost-aware accepting prefix--suffix waypoint plan executed by the frozen executor. This separation of learning and planning enables zero-shot generalization to unseen LTL formulas and new predicates supported by the offline data, without task-specific rewards, additional data collection, or policy retraining. Experiments on LTL task suites constructed from OGBench locomotion domains show that SAGAS achieves higher success rates and lower execution costs than baselines on diverse unseen tasks, with further evaluation in OGBench Scene demonstrating its applicability to robotic manipulation.