Pith. sign in

REVIEW 3 major objections 5 minor 35 references

STeP: Signal Temporal Logic for Precise Specifications for Action Generation with Vision Language Models

T0 review · 3 major / 5 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper claims that translating natural-language robot instructions into Signal Temporal Logic specifications, then using those formulas for control, monitoring, and replanning, lets robots satisfy spatial, temporal, and logical constrai

desk verdict A genuinely useful architectural idea — STL as a persistent formal layer between VLM planning and low-level execution — with real-robot experiments, but the headline claim rests on an undefined success metric that may be circular. read the letter →

arxiv 2607.18580 v1 pith:VNE2N3OA submitted 2026-07-20 cs.RO

Kasra Torshizi , Anukriti Singh , Sidharth Mathur , Khuzema Habib , Leo Du , Pratap Tokekar This is my paper
classification cs.RO
keywords SignalTemporalLogicvision-language-actionmodelsrobottaskplanningmodelpredictivecontrolmanipulationruntimemonitoringreplanningformalspecifications
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper argues that a robot following natural-language instructions needs an explicit formal layer between high-level language understanding and low-level motor control, not just a learned policy that is expected to absorb all constraints implicitly. It proposes Signal Temporal Logic (STL) as that layer: a vision-language model decomposes instructions into subtasks and compiles each into an STL formula, which then guides model-predictive control, is monitored during execution, and structures replanning after failures. In real-world tabletop experiments with a UR3e arm, the STL-based system achieved higher 'safe success rates' than a baseline using direct MPC cost functions across spatial, temporal, and logical constraint tasks, with the largest gains on temporal constraints. It also used STL robustness as a switching signal to move control from a learned policy to MPC when a collision loomed, and used STL violation traces to correct most stacking failures within three attempts. If correct, the framework makes language-conditioned robots more precise, safer, and more interpretable without sacrificing task completion.

What carries the argument

The load-bearing object is the STL specification itself, evaluated through quantitative robustness semantics. A deterministic compiler turns each VLM-generated subtask template into an STL formula over a predefined predicate library (e.g., Safe(region), GoalPosition, Grasp), where predicates map state and observation signals to real-valued margins; robustness scores are smoothed with a softmax min/max approximation so they can feed gradient-based MPC optimization. The same formula then supports three jobs: as a cost term in MPC, as a completion/violation monitor during execution, and as structured feedback (which predicate failed, by what margin, at what time) that anchors replanning to the

What would settle it

Re-run the nine RQ1 tasks after deliberately offsetting all object poses by a known amount along the camera axis (e.g., +2 cm depth bias) while keeping the rest of the pipeline fixed; if the reported safe success rates do not degrade correspondingly, the predicates are not actually tracking the physical constraints they name.

Watch

Extended reading notes

Core claim

The paper claims that translating natural-language instructions into Signal Temporal Logic specifications—rather than leaving spatial, temporal, and logical requirements implicit in a VLA policy—lets a robot check, optimize, monitor, and revise its own behavior with one formal structure. System 2 (a VLM) turns each instruction into a validated sequence of subtasks paired with STL formulas over a predicate library; System 1 executes each subtask with either STL-guided MPC or a learned policy, while an STL monitor computes robustness scores for completion and violation. The experiments report higher safe success rates on nine real tabletop tasks compared to an ablated baseline, successful runt

Load-bearing premise

The loop reads the world through object poses and distances estimated from a single camera with a depth sensor; if those estimates are biased, the STL predicates—and the monitor, MPC costs, and success scores built on them—are evaluating a false world model.

Editorial extensions

If this is right

  • STL-guided planning improves constraint satisfaction across logical, spatial, and temporal task types on a real UR3e arm, with the largest gains on temporal constraints, while overall task success is not sacrificed.
  • STL robustness can serve as a runtime switching signal: monitoring a learned policy and handing control to MPC when safety robustness drops prevents collisions and preserves grasp success.
  • Structured STL violation traces (violated predicate, robustness margin, timestep) enable more targeted replanning than scalar cost feedback, correcting most stacking failures within three attempts.
  • A persistent formal task specification keeps replanning grounded in the original instruction rather than regenerating from scratch.
  • Formalization makes language-derived plans checkable and interpretable at runtime.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the same architecture could enforce constraints during learned-policy inference by feeding robustness gradients into the policy, closing the gap the paper notes between monitoring and direct enforcement.
  • Editorial inference: a sequence-of-subtasks plan limits branching and cyclic tasks; extending the STL representation to automata-style plans is the obvious next test of the framework's reach.
  • Editorial inference: because the monitor and the success metric share the same perception pipeline, the reported gains are upper bounds tied to perception accuracy; a cleaner evaluation would separate perception error from planning error.
  • Editorial inference: the robustness trace doubles as a diagnostic—recording which predicate failed and when could support automatic debugging of VLM-generated specifications in cluttered scenes.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 5 minor

Summary. The paper proposes STeP, a hierarchical framework that uses Signal Temporal Logic (STL) as an interface between a VLM-based high-level planner (System 2) and low-level execution (System 1) for tabletop manipulation. System 2 decomposes natural-language instructions into subtasks and compiles each into STL formulas over a predefined predicate library; System 1 executes these via STL-guided MPC or learned policies, with STL robustness used for monitoring, switching, and replanning. The evaluation reports real-robot results on nine tabletop tasks grouped by constraint type (Figure 4), a switching experiment with 30 trials (RQ2), and a replanning experiment with 20 trials (RQ3), comparing against a VLM-MPC-COST ablation without STL. The central claim is that STL-guided planning yields more reliable satisfaction of spatial, temporal, and logical constraints without sacrificing task performance.

Significance. If the empirical claims hold, the paper makes a useful contribution: it demonstrates a complete closed-loop instantiation of STL as a persistent formal layer between language-level task reasoning and real-robot execution, including monitoring-driven switching and structured replanning feedback. Strengths include real-hardware evaluation (UR3e), clearly stated limitations, and a design that makes the role of STL in each pipeline stage explicit. The comparison against an ablation that replaces STL with scalar MPC costs is a reasonable way to isolate the effect of the formal structure, and the RQ3 design (structured vs scalar failure feedback) is a sensible test of the claimed advantage of STL traces. The paper does not overclaim beyond its evaluation scope and identifies key weaknesses (e.g., learned policies are only monitored, not optimized; perception is a single RGB-D capture).

major comments (3)
  1. [§5.1, Figure 4] RQ1's headline result is carried entirely by 'safe success rates' in Figure 4, yet the paper never defines how a safe success is scored. If the score is derived from the same perception signals z_t=ψ(s_t,o_t) used in the STL predicates, MPC costs, and monitor (App. 8.4), then the comparison with VLM-MPC-COST partly measures how well each method optimizes the same proxy rather than the user-intended physical constraints. The paper reports no independent ground truth (e.g., motion capture, human labels, or pose-error analysis) for the nine tasks. I request a precise definition of the safe-success label and, if it is a function of the STL monitor or perception estimates, an explicit acknowledgment of this coupling plus at least a small validation (e.g., manual labeling or measured placement error) for a subset of trials.
  2. [§5.1, Figure 4; §5.2; §5.3] None of the experimental results include per-condition trial counts or variance/error information. Figure 4 aggregates 'across nine tasks' with no per-task counts, and RQ2/RQ3 report only point estimates (e.g., 22/30, 14/16). Since the claimed gains are empirical and the effect sizes are not reported as distributions, I cannot judge whether the differences are meaningful. Please report per-task or per-condition trial counts, raw success numbers, and where feasible error bars or confidence intervals; if trials are not repeated, state that explicitly.
  3. [§4.2.2, Eq. (1)] The MPC objective uses the current observation o_t to compute predicted signals z_{k|t}=ψ(s_{k|t},o_t) for the entire look-ahead horizon. Since the robot moves relative to objects, future predicate values (e.g., distances to movable objects) can be wrong if the observer or the world changes. The authors note this in Limitations, but it is load-bearing for the RQ1 claim because the monitor and MPC then act on potentially biased signals for all tasks involving object-relative goals. I would like a sensitivity discussion or a simple experiment quantifying how robustness values or success rates change with perception error (e.g., artificial pixel/depth perturbations), or at minimum an explicit statement of which tasks are robust to this approximation because the relevant objects are static during the subtask.
minor comments (5)
  1. [§5.1, Figure 4] The y-axis label says 'safe success rate' but the text and caption do not define it. Please add a definition in the caption or main text.
  2. [§4.1] The 'flexible GoalPosition predicate' is introduced as a catch-all for cases where the predefined library is insufficient. Since this predicate appears to be defined by the VLM and may not be differentiable or semantically grounded, please clarify how its robustness is computed and whether any RQ1 task used it; if used, explain how that affects the claim that the library is predefined.
  3. [§5.3] The text says '12 of the 16 failures are corrected on the second attempt and 14 are corrected within three attempts' after reporting 16/20 initial failures, but it is unclear whether the 14 within three attempts includes the 12 second-attempt successes or refers to trials not yet recovered. Please clarify the accounting.
  4. [§2] The related-work section could better position this paper relative to recent NL-to-STL translation with verification (Ref. [31]) and to STL-based MPC works (Refs. [24, 7]); the current text is adequate but a sentence distinguishing the closed-loop monitoring/replanning use from prior verification-only use would help.
  5. [Eq. (1)] The softmax approximation β is listed as a free parameter; please state the value used in experiments and whether results are sensitive to it.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the central claims are empirical comparisons against an ablation, and the only self-citation is non-load-bearing.

full rationale

The paper's main claims (RQ1, RQ2, RQ3) are empirical evaluations on a real UR3e platform against an ablated baseline (VLM-MPC-COST), not derivations from fitted parameters or first-principles results. The STL specifications are produced by a deterministic compiler from the authors' own skill templates, with the VLM selecting from a predefined predicate library; no parameter is fitted to a subset of data and then renamed as a prediction. The only self-citation is [11] (PlanRL, with author Tokekar), used in the introduction to motivate hybrid learned-policy/MPC execution and STL monitoring; it is not load-bearing and no uniqueness theorem or ansatz is imported from prior author work. The paper's own limitations—struggling in cluttered environments (§7), predicting future signals with the current observation o_t rather than future observations (§4.2.2), and the possibility of incorrect VLM-generated specifications (§7)—are threats to external validity but not to circularity. One evaluation concern is that the 'safe success rates' in Figure 4 are not defined in the text; if they were computed from the same STL monitor used for completion detection, RQ1 would be partly circular, but the paper does not state this, so flagging it as a circular step would be speculation. No circular step can be exhibited from the text's equations or citations.

Assumptions & free parameters 4 free parameters · 5 assumptions · 1 invented entities

The ledger shows the framework's true intellectual cost: the formal layer is anchored by hand-authored compiler templates and a hand-built predicate library (ad hoc), by the assumption that a proprietary VLM formalizes instructions correctly (which the authors concede fails in some cases), and by perceptual pose estimates from a single RGB-D capture. The STL mathematics themselves are standard prior work (standard_math). No cosmic entities are introduced; the one escape hatch is the flexible GoalPosition predicate. The hand-tuned MPC/monitor hyperparameters (lambda, beta, thresholds, horizon) are unspecified in the text.

free parameters (4)
  • MPC robustness weight lambda
    Weights STL robustness against nominal cost in the MPC objective (§4.2.2, Eq. 1); value not reported, presumably hand-tuned.
  • Softmax sharpness beta
    Controls the smooth max/min approximation used for differentiable robustness (§3.3); value not reported.
  • STL recall threshold and MPC horizon H
    Robustness level below which System 1 triggers recall (§4.2) and finite-horizon length for MPC (§4.2.2); values not reported and presumably task-dependent.
  • Per-task predicate thresholds and timing windows (8 cm offset, [5,8] s interval, safe-distance margins) = chosen per instruction by GPT-4o
    These numbers define the STL atomic predicates against which success is judged (§3.2, Fig. 1). They come from the language instruction rather than being fit to data, but they are free choices that directly determine trial outcomes.
assumptions (5)
  • standard math STL syntax and quantitative robustness semantics (Table 1), including the soft-max smooth approximation.
    Standard results from Maler/Nickovic, Donze/Maler, and Fainekos/Pappas, adopted without proof (§3, App. 8.1).
  • domain assumption GPT-4o returns valid, schema-conforming subtask sequences and parameter bindings from language plus scene context.
    The entire pipeline's formalization quality depends on this; the authors admit in Limitations that 'the VLM can still produce incomplete or incorrect task specifications.'
  • ad hoc to paper The hand-authored skill-to-STL compiler templates and the predefined predicate library faithfully encode the constraints in the language instruction.
    The mapping from each skill template to an STL formula is designed by the authors (§4.1, §3.2); wrong or incomplete templates formalize the wrong constraint while giving an impression of correctness.
  • domain assumption A dynamics model f for the arm exists and is accurate enough that MPC-predicted trajectories' robustness reflects executed behavior.
    MPC optimizes robustness over predicted signals computed 'using the predicted states and the current observation o_t' (§4.2.2); the authors themselves note future observations are not predicted.
  • domain assumption Perception from a single RGB-D capture (SAM + VLM labeling + depth back-projection) yields accurate world-frame poses for all entities used in predicates.
    STL monitoring and the 'safe success' metric rely on measured signals z_t = psi(s_t, o_t) (App. 8.4); metric predicates are only as accurate as perception.
invented entities (1)
  • 'Flexible GoalPosition predicate' — catch-all signal predicate appended to the predefined library
    purpose: Allows the VLM to express goal constraints not covered by the library, at the cost of the formal specification becoming arbitrary VLM output rather than a library-defined signal
    Introduced as an escape hatch in §3.2 ('although we add in a flexible GoalPosition predicate in case defined predicates do not suffice'); its semantics are whatever the VLM emits, which weakens the claim that constraints are formally grounded.

how reviews work

0 comments
Cite this review

Pith. "Pith review of STeP: Signal Temporal Logic for Precise Specifications for Action Generation with Vision Language Models." pith.science (2026). https://pith.science/paper/VNE2N3OA

@misc{pith2026260718580,
  author       = {Pith},
  title        = {Pith review of: STeP: Signal Temporal Logic for Precise Specifications for Action Generation with Vision Language Models},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VNE2N3OA}},
  note         = {Machine review of arXiv:2607.18580}
}
read the original abstract

Vision-language-action (VLA) models have shown impressive generalization, but often lack interpretability and can struggle to follow precise natural language instructions that encode spatial, temporal, and logical requirements. We propose a hierarchical framework that uses Signal Temporal Logic (STL) as a shared representation connecting high-level language understanding with low-level robot execution. A high-level policy leverages a VLM to decompose language instructions into high-level subtasks, generate STL specifications for each subtask, and choose a low-level policy for executing each subtask. The STL specifications translate language-derived intent into precise constraints, and the low-level policy selection determines whether those constraints are enforced directly through STL-guided model-predictive control or monitored during execution of a learned policy for perceptually complex, or contact-rich behaviors. By integrating STL into plan validation, low-level policy, subtask monitoring, and replanning, our framework enables language-derived plans to be checked, optimized, and revised at runtime using a common formal structure. We evaluate the approach on a real-world tabletop domain, demonstrating how formal specifications can improve the precision, reliability, and interpretability of language-conditioned robot planning.

Figures

Figures reproduced from arXiv: 2607.18580 by the authors.

Figure 1
Figure 1. A single language instruction can encode temporal (“within 5 to 8 seconds”) and spatial [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
Figure 2
Figure 2. Overview of STEP. System 2 uses the language instruction, current observation, skill library, and history log to decompose the task into subtasks and compile each subtask into an STL specification. System 1 executes the active subtask using the selected low-level policy or controller, while STL monitoring tracks progress and detects failures. Upon subtask completion or violation, the history log provides recall cont… view at source ↗
Figure 3
Figure 3. In-depth showcase of key components of our pipeline. a) Depicts how we construct a [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figures from the paper (3 more)
Figure 4
Figure 4. Figure 4: Real World Results of our method compared to VLM-MPC-C [PITH_FULL_IMAGE:figures/full_fig_p007_4.png]
Figure 5
Figure 5. Figure 5: Yellow: learned policy path. Red: projected continua￾tion. Blue: intervention point. Green: MPC recovery. We evaluate whether STL violation traces enable more targeted plan cor￾rections than informal failure feedback. The system is instructed to stack three cubes, wher…
Figure 6
Figure 6. Figure 6: Detailed views of the two modules in STEP. System 2 converts language, scene context, skill definitions, and recall context into an STL-annotated task specification. System 1 executes each subtask through either STL-guided MPC or a learned policy, while STL monitoring …

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

35 extracted references · 1 canonical work pages

  1. [1]

    Bjorck, F

    NVIDIA, :, J. Bjorck, F. Casta ˜neda, N. Cherniadev, X. Da, R. Ding, L. J. Fan, Y . Fang, D. Fox, F. Hu, S. Huang, J. Jang, Z. Jiang, J. Kautz, K. Kundalia, L. Lao, Z. Li, Z. Lin, K. Lin, G. Liu, E. Llontop, L. Magne, A. Mandlekar, A. Narayan, S. Nasiriany, S. Reed, Y . L. Tan, G. Wang, Z. Wang, J. Wang, Q. Wang, J. Xiang, Y . Xie, Y . Xu, Z. Xu, S. Ye, Z...

    arXiv 2025

  2. [2]

    C. Cui, P. Ding, W. Song, S. Bai, X. Tong, Z. Ge, R. Suo, W. Zhou, Y . Liu, B. Jia, H. Zhao, S. Huang, and D. Wang. Openhelix: A short survey, empirical analysis, and open-source dual- system vla model for robotic manipulation, 2025. URLhttps://arxiv.org/abs/2505. 03912

    2025

  3. [3]

    B. Han, J. Kim, and J. Jang. A dual process vla: Efficient robotic manipulation leveraging vlm,

  4. [4]

    Maler and D

    O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals. In Y . Lakhnech and S. Yovine, editors,Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, pages 152–166, Berlin, Heidelberg, 2004. Springer Berlin Heidelberg. ISBN 978-3-540-30206-3

    2004

  5. [5]

    G. E. Fainekos and G. J. Pappas. Robustness of temporal logic specifications for continuous- time signals.Theoretical Computer Science, 410(42):4262–4291, 2009. ISSN 0304-3975. doi:https://doi.org/10.1016/j.tcs.2009.06.021. URLhttps://www.sciencedirect.com/ science/article/pii/S0304397509004149

    doi:10.1016/j.tcs.2009.06.021 2009

  6. [6]

    Donz ´e and O

    A. Donz ´e and O. Maler. Robust satisfaction of temporal logic over real-valued signals. In Formal Modeling and Analysis of Timed Systems, volume 6246 ofLecture Notes in Computer Science, pages 92–106. Springer, 2010. doi:10.1007/978-3-642-15297-9 9

    doi:10.1007/978-3-642-15297-9 2010

  7. [7]

    Sadraddini and C

    S. Sadraddini and C. Belta. Robust temporal logic model predictive control. InProceedings of the 53rd Annual Allerton Conference on Communication, Control, and Computing, pages 772–779. IEEE, 2015. doi:10.1109/ALLERTON.2015.7447084

    arXiv 2015

  8. [8]

    M. J. Kim, K. Pertsch, S. Karamcheti, T. Xiao, A. Balakrishna, S. Nair, R. Rafailov, E. Foster, G. Lam, P. Sanketi, Q. Vuong, T. Kollar, B. Burchfiel, R. Tedrake, D. Sadigh, S. Levine, P. Liang, and C. Finn. Openvla: An open-source vision-language-action model, 2024. URL https://arxiv.org/abs/2406.09246

    arXiv 2024

Show all 35 references
  1. [9]

    M. J. Kim, C. Finn, and P. Liang. Fine-tuning vision-language-action models: Optimizing speed and success, 2025. URLhttps://arxiv.org/abs/2502.19645

    2025 arXiv

  2. [10]

    Li, C.-I

    X. Li, C.-I. Vasile, and C. Belta. Reinforcement learning with temporal logic rewards, 2017. URLhttps://arxiv.org/abs/1612.03471

    2017 arXiv

  3. [11]

    Bhaskar, Z

    A. Bhaskar, Z. Mahammad, S. R. Jadhav, and P. Tokekar. Planrl: A motion planning and imitation learning framework to bootstrap reinforcement learning, 2024. URLhttps: //arxiv.org/abs/2408.04054

    2024 arXiv

  4. [12]

    Belkhale, Y

    S. Belkhale, Y . Cui, and D. Sadigh. Hydra: Hybrid robot actions for imitation learning, 2023. URLhttps://arxiv.org/abs/2306.17237. 9

    2023 arXiv

  5. [13]

    M. Ahn, A. Brohan, N. Brown, Y . Chebotar, O. Cortes, B. David, C. Finn, C. Fu, K. Gopalakr- ishnan, K. Hausman, A. Herzog, D. Ho, J. Hsu, J. Ibarz, B. Ichter, A. Irpan, E. Jang, R. J. Ruano, K. Jeffrey, S. Jesmonth, N. J. Joshi, R. Julian, D. Kalashnikov, Y . Kuang, K.-H. Lee...

  6. [14]

    Singh, V

    I. Singh, V . Blukis, A. Mousavian, A. Goyal, D. Xu, J. Tremblay, D. Fox, J. Thomason, and A. Garg. Progprompt: Generating situated robot task plans using large language models, 2022. URLhttps://arxiv.org/abs/2209.11302

    2022 arXiv

  7. [15]

    Liang, W

    J. Liang, W. Huang, F. Xia, P. Xu, K. Hausman, B. Ichter, P. Florence, and A. Zeng. Code as policies: Language model programs for embodied control, 2023. URLhttps://arxiv. org/abs/2209.07753

    2023 arXiv

  8. [16]

    Huang, C

    W. Huang, C. Wang, R. Zhang, Y . Li, J. Wu, and L. Fei-Fei. V oxposer: Composable 3d value maps for robotic manipulation with language models, 2023. URLhttps://arxiv.org/abs/ 2307.05973

    2023 arXiv

  9. [17]

    Huang, C

    W. Huang, C. Wang, Y . Li, R. Zhang, and L. Fei-Fei. Rekep: Spatio-temporal reasoning of relational keypoint constraints for robotic manipulation, 2024. URLhttps://arxiv.org/ abs/2409.01652

    2024 arXiv

  10. [18]

    Singh, R

    H. Singh, R. J. Das, M. Han, P. Nakov, and I. Laptev. Malmm: Multi-agent large language models for zero-shot robotics manipulation, 2025. URLhttps://arxiv.org/abs/2411. 17636

    2025

  11. [19]

    Liu, A.-C

    I. Liu, A.-C. Cheng, R. Yan, G. Chen, R.-Z. Qiu, X. Zou, S. Yi, H. Yin, X. Wang, and S. Liu. Long-horizon manipulation via trace-conditioned vla planning, 2026. URLhttps://arxiv. org/abs/2604.21924

    2026 arXiv

  12. [20]

    Kress-Gazit, G

    H. Kress-Gazit, G. E. Fainekos, and G. J. Pappas. Temporal-logic-based reactive mission and motion planning.Trans. Rob., 25(6):1370–1381, Dec. 2009. ISSN 1552-3098. doi: 10.1109/TRO.2009.2030225. URLhttps://doi.org/10.1109/TRO.2009.2030225

    2009

  13. [21]

    Kloetzer and C

    M. Kloetzer and C. A. Belta. A fully automated framework for control of linear systems from temporal logic specifications.IEEE Transactions on Automatic Control, 53:287–297, 2008. URLhttps://api.semanticscholar.org/CorpusID:15975471

    2008

  14. [22]

    Kress-Gazit, T

    H. Kress-Gazit, T. Wongpiromsarn, and U. Topcu. Correct, reactive robot control from ab- straction and temporal logic specifications. 09 2014

    2014

  15. [23]

    Wells and E

    A. Wells and E. Plaku. Adaptive sampling-based motion planning for mobile robots with dif- ferential constraints. In C. Dixon and K. Tuyls, editors,Towards Autonomous Robotic Systems, pages 283–295, Cham, 2015. Springer International Publishing. ISBN 978-3-319-22416-9

    2015

  16. [24]

    Raman, A

    V . Raman, A. Donz ´e, M. Maasoumy, R. M. Murray, A. Sangiovanni-Vincentelli, and S. A. Seshia. Model predictive control with signal temporal logic specifications. InProceedings of the 53rd IEEE Conference on Decision and Control, pages 81–87. IEEE, 2014. doi:10.1109/ CDC.2014.7039363

    2014

  17. [25]

    S. S. Farahani, S. E. Zadeh Soudjani, R. Majumdar, and C. Ocampo-Martinez. Robust model predictive control with signal temporal logic constraints for barcelona wastewater system. IFAC-PapersOnLine, 50(1):6594–6600, 2017. ISSN 2405-8963. doi:https://doi.org/10.1016/ j.ifacol.20...

    2017

  18. [26]

    Kapoor, K

    P. Kapoor, K. Mizuta, E. Kang, and K. Leung. Stlcg++: A masking approach for differentiable signal temporal logic specification.IEEE Robotics and Automation Letters, 10(9):9240–9247,

  19. [27]

    Leung, N

    K. Leung, N. Ar ´echiga, and M. Pavone. Backpropagation through signal temporal logic specifications: Infusing logical structure into gradient-based methods, 2021. URLhttps: //arxiv.org/abs/2008.00097

    2021 arXiv

  20. [28]

    J. He, E. Bartocci, D. Ni ˇckovi´c, H. Isakovic, and R. Grosu. Deepstl – from english require- ments to signal temporal logic, 2022. URLhttps://arxiv.org/abs/2109.10294

    2022 arXiv

  21. [29]

    Y . Mao, T. Zhang, X. Cao, Z. Chen, X. Liang, B. Xu, and H. Fang. Nl2stl: Transformation from logic natural language to signal temporal logics using llama2.Proceedings of the IEEE International Conference on Cybernetics and Intelligent Systems, CIS, (2024):469–474, 2024. ISSN ...

    2024

  22. [30]

    Y . Fang, Z. Jin, J. An, H. Chen, X. Chen, and N. Zhan. Enhancing transformation from natural language to signal temporal logic using llms with diverse external knowledge, 2025. URL https://arxiv.org/abs/2505.20658

    2025 arXiv

  23. [31]

    J. Choi, K. A. Pant, K. Nune, and I. Hwang. Reachability-based temporal logic verification for reliable llm-guided human-autonomy teaming, 2026. URLhttps://arxiv.org/abs/ 2603.08633

    2026

  24. [32]

    Bartocci, J

    E. Bartocci, J. Deshmukh, A. Donz ´e, G. Fainekos, O. Maler, D. Nickovic, and S. Sankara- narayanan.Specification-Based Monitoring of Cyber-Physical Systems: A Survey on The- ory, Tools and Applications, pages 135–175. 02 2018. ISBN 978-3-319-75631-8. doi: 10.1007/978-3-319-75...

    2018 doi

  25. [2022]

    URLhttps://arxiv.org/abs/2204.01691

    arXiv

  26. [2024]

    URLhttps://arxiv.org/abs/2410.15549

    arXiv

  27. [2025]

    doi:10.1109/lra.2025.3588389

    ISSN 2377-3774. doi:10.1109/lra.2025.3588389. URLhttp://dx.doi.org/10. 1109/LRA.2025.3588389

    2025

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.