Pith. sign in

REVIEW 3 major objections 5 minor 4 cited by

The paper introduces SENTINEL, a framework that formally evaluates the physical safety of LLM-based embodied agents by grounding natural-language safety requirements in LTL and CTL and verifying them across semantic, plan, and trajectory le

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

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

T0 review · deepseek-v4-flash

2026-08-04 09:48 UTC pith:3XW7JI4S

load-bearing objection Useful multi-level safety evaluation framework, but the 'all potential outcomes' claim at the trajectory level is not supported by five sampled rollouts; fix the language or add coverage arguments. the 3 major comments →

arxiv 2510.12985 v3 pith:3XW7JI4S submitted 2025-10-14 cs.AI

SENTINEL: A Multi-Level Formal Framework for Safety Evaluation of Foundation Model-based Embodied Agents

Simon Sinong Zhan , Philip Wang , Yao Liu , Yiyan Peng , Zinan Wang , Qineng Wang , Zhian Ruan , Xiangyu Shi
show 8 more authors
Xinyu Cao Frank Yang Zhenyang Ni Kangrui Wang Ruohan Zhang Huajie Shao Manling Li Qi Zhu
This is my paper
classification cs.AI
keywords embodied agentssafety evaluationtemporal logicLTLCTLmodel checkingLLM planningformal verification
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

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

SENTINEL claims to be the first framework that evaluates physical safety of LLM-based embodied agents formally, rather than with heuristic rules or subjective LLM judges. It converts natural-language safety requirements into LTL formulas, then checks three levels: whether the LLM understands the formalized constraint, whether its high-level plan satisfies the LTL constraints, and whether executed trajectories—merged into a computation tree—satisfy CTL specifications. The payoff is a diagnostic tool that can attribute a safety failure to misinterpretation, unsafe planning, or unsafe execution, and that returns counterexamples pinpointing the violation.

Core claim

Grounding safety in temporal logic and applying verification at three levels makes safety evaluation of embodied LLM agents formal and attributable. At the semantic level, LLM-generated LTL formulas are compared against ground truth for logical equivalence via automata-based containment. At the plan level, high-level subgoal plans are checked against LTL. At the trajectory level, multiple sampled executions are merged into a computation tree and checked with CTL operators, so hazards invisible at the plan level—collisions, proximity violations, ordering hazards—are caught. Experiments in two household simulation environments show the pipeline operates across simulators and exposes violations

What carries the argument

Temporal logic (LTL and CTL) carried by a three-stage pipeline. Natural-language safety rules are formalized into LTL; a satisfiability-based automata check tests whether an LLM's translation is semantically equivalent to ground truth. Plans are verified against LTL. Executions are sampled, merged into a branching computation tree, and checked with CTL operators (AG, AF, AX, AU); the universal path quantifier is what lets the framework claim to evaluate 'all' outcomes. A curated safety database of object categories instantiates general constraint templates into scene-specific formulas.

Load-bearing premise

The framework's claim to check all possible execution outcomes rests on treating a small set of sampled trajectories as standing in for every behavior the agent could produce; if a violating branch lies outside the sample, the safety verdict is wrong despite a clean check.

What would settle it

Run SENTINEL on a small task with a known unsafe branch, but sample only safe trajectories; if the framework reports a CTL pass while an exhaustive enumeration of the agent's action sequences includes a violating branch, the 'all potential execution outcomes' claim is refuted.

Watch this falsifier — get emailed when new claim-graph text bears on it.

If this is right

  • Safety evaluation no longer depends on subjective LLM judgments; the same LTL/CTL specification serves as an objective yardstick.
  • Failures can be attributed to one of three levels, guiding whether to fix interpretation, planning, or low-level control.
  • Because constraints are expressed in temporal logic, the framework extends naturally to timed and continuous safety properties.
  • The computation-tree representation allows newly collected trajectories to be added and rechecked without re-verifying each path independently.
  • The safety database and template instantiation make the framework portable across simulators that provide object metadata.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The 'all paths' guarantee is only as strong as the sampled trajectories; a straightforward extension is to report the CTL verdict as a coverage-bounded claim or to couple sampling with statistical guarantees.
  • The semantic-level equivalence check could be repurposed as a training signal: feeding counterexample words from the automata back to the LLM would give it concrete corrections about what its translated formula gets wrong.
  • The same multi-level decomposition could be used for runtime monitoring: instead of only evaluating after the fact, the LTL/CTL specifications could be compiled into shields that block unsafe actions during execution.
  • Because the framework attributes failures to levels, benchmark results across models can be read as a roadmap of where model capability matters most—semantic interpretation, planning, or low-level control.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper presents SENTINEL, a multi-level framework for evaluating the safety of LLM-based embodied agents. It formalizes natural-language safety requirements in LTL/CTL, then evaluates agents progressively at three levels: semantic interpretation (whether the LLM translates NL safety rules into LTL formulas that are logically equivalent to ground-truth constraints), plan-level safety (whether high-level plans satisfy the LTL constraints), and trajectory-level safety (whether simulated execution trajectories, merged into a computation tree, satisfy CTL safety properties). The framework is instantiated in VirtualHome and ALFRED/AI2-THOR and tested across several closed- and open-source LLMs. The central claimed contribution is that SENTINEL is the first framework to formally evaluate physical safety across semantic, plan, and trajectory levels and that its CTL-based trajectory check ensures safety across all potential execution outcomes.

Significance. If the formal claims were fully supported, SENTINEL would be a valuable step beyond current embodied-agent safety benchmarks: it replaces LLM-as-judge with automata-theoretic semantic equivalence and explicit CTL model-checking algorithms, and its progressive multi-level design could help attribute safety failures to interpretation, planning, or execution. The pseudocode for the checking algorithms and the use of Büchi automata for semantic equivalence are concrete, reproducible contributions. However, the trajectory-level guarantee is the key differentiator and, as argued below, that guarantee is not currently established. The empirical protocol also has design issues that complicate interpretation of the reported violation rates. The multi-level architecture and the semantic/plan-level formalization are defensible, but the strongest claims need revision before publication.

major comments (3)
  1. [Section 2.3 / Algorithm 6 / Section 3.3] The paper states at the end of Section 2.3 that SENTINEL 'ensures that safety is evaluated across all potential execution outcomes.' This is the central formal claim, but it is not supported by the construction. Algorithm 6 builds the computation tree T from n trajectories, and Section 3.3 fixes n=5 per task (Table 4). The CTL universal quantifier A therefore ranges only over the branches observed in those five samples, not over the full state-transition behavior of the LLM+simulator system. No simulation relation, bisimulation, or coverage argument is given to connect T to the actual set of possible executions. Consequently T,s0 |= AG φ does not imply that no unsafe execution exists; it only says that no violation was observed in the sample. This directly contradicts the abstract and the Section 2.3 claim. To make the formal guarantee load-bearing, the authors should either prove a cove
  2. [Section B.3 / Section 3.3] The trajectory-level hazard injection protocol is problematic. Section B.3 says hazards are injected 'based on the generated trajectory' and 'manually inject hazards along the agent's path and/or at the target end position.' This means the evaluation scenario is chosen with knowledge of the agent's output, after the agent has acted. As a result, the safety rates in Table 4 do not measure how well an agent avoids hazards under a fixed, fair condition; they measure responses to adversarially selected hazards. Furthermore, the same task is not evaluated under identical hazard conditions across models, so the model comparisons in Table 4 are hard to interpret. This does not invalidate the framework's potential as a diagnostic tool, but it weakens the empirical evidence for the claim that SENTINEL 'effectively expose[s] potential safety violations.' The authors should re-run the evaluation wi
  3. [Section 2.3 / Algorithm 6 (tree construction)] The construction of the computation tree T from multiple sampled trajectories is not formally defined. How are states from different trajectories identified or merged? If two trajectories diverge and later reconverge, is state equality based on the raw simulator state, on the labeled atomic propositions, or on some abstraction? Without a definition of the state space and transition relation used for the tree, the CTL semantics is ambiguous even for the sampled branches. The paper should define T precisely: the underlying state equivalence, how branches are attached, and what the transition relation R contains. This is needed for the formal claim regardless of whether the tree represents all possible executions.
minor comments (5)
  1. [Section 2.2 / Appendix B.1] The objects labeled 'Theorem 2.2' and 'Theorem B.1' are examples, not theorems. This mislabeling recurs in Figure 2, Figure 3, and the text around Example 2.3 and should be corrected.
  2. [Algorithm 6] Algorithm 6 loops 'for i in [0,n]' and then calls GenerateAction and GenerateTraj, which suggests n+1 trajectories if n is the number of samples. Section 3.3 says 'five execution trials for each task.' Clarify the indexing so the sample size is unambiguous.
  3. [Section D.3.3] The description of AU reads 'ψ should holeTrue until ψ holdsTrue.' This is a typo; it should say 'ϕ should hold until ψ holds.'
  4. [Section 3.3 / Table 4] The sentence 'we sample five execution trials for each task,.' has a stray comma. More importantly, with n=5 per task, the safety and success percentages in Table 4 are likely to have wide confidence intervals; reporting standard errors or per-task breakdowns would help the reader assess the reliability of the comparisons.
  5. [Section B.2] The ground-truth LTL constraints are generated from the authors' own safety templates and object-property database. This is reasonable for a benchmark, but the semantic-level equivalence results should be interpreted as measuring alignment with this particular safety ontology, not as a general measure of 'safety understanding.' A sentence acknowledging this limitation would improve the presentation.

Circularity Check

0 steps flagged

No significant circularity: the formal evaluation pipeline is self-contained; the trajectory-level 'all outcomes' claim is a coverage gap, not a circular reduction.

full rationale

SENTINEL's central contribution is a benchmark/protocol, not a derived theorem. The ground-truth LTL/CTL constraints are human-curated from a safety database and general templates (Section B.2), independently of the LLM outputs being evaluated; no parameter is fitted from the target data and no 'prediction' is constructed from the quantity it claims to test. Semantic-level equivalence checking uses automata-theoretic language containment against this curated ground truth; plan-level and trajectory-level checks evaluate generated plans/trajectories against the same externally fixed formulas. The only step that might look like an equivocation is the trajectory-level claim that checking the sampled computation tree 'ensures that safety is evaluated across all potential execution outcomes' (end of Section 2.3). Algorithm 6 builds T from n sampled trajectories (Section 3.3: 'we sample five execution trials for each task'), so the CTL universal quantifier ranges over the observed sample, not the full behavior space. This is an overclaim/coverage gap, not a circularity: the model-checking result is not defined in terms of the conclusion, and the paper explicitly disclaims exhaustiveness ('These experiments are not intended as a comprehensive benchmark...' in Section 3; 'Admittedly, this work is not intended as an exhaustive benchmark...' in Section B.3). Self-citations (e.g., Mars, Zhan et al. 2024a) appear only as optional future tooling, not as load-bearing support. No fitted parameter, no uniqueness theorem, and no ansatz is smuggled in via citation. Score 0.

Axiom & Free-Parameter Ledger

2 free parameters · 5 axioms · 0 invented entities

The framework rests on standard temporal-logic semantics plus author-curated safety templates and simulator abstractions. There are no free constants inside the formal logic itself, but hand-set thresholds and finite sampling budgets shape what counts as a violation and how comprehensive the check is.

free parameters (2)
  • safe-distance threshold r_hazard = 0.5 units (kettle–phone example)
    Hand-chosen spatial threshold used to define trajectory-level safety violations; different thresholds change which trajectories are flagged unsafe.
  • number of sampled trajectories n = 5 per task
    Hand-selected sampling budget; the claim of evaluating all potential outcomes depends on this finite sample, making it a load-bearing experimental parameter.
axioms (5)
  • standard math LTL/CTL satisfaction semantics (Pnueli 1977; Clarke & Emerson 1981) are the correct formal semantics for the safety properties considered.
    The framework directly adopts standard temporal logic definitions.
  • domain assumption Object metadata and PDDL state transitions in VirtualHome and ALFRED faithfully capture safety-relevant physical states and actions.
    Trajectory-level checking operates on simulator states; if the simulator omits physical details (e.g., exact distances, collision geometry), the CTL results may miss real hazards.
  • domain assumption The author-curated safety database and LTL templates are correct and sufficient formalizations of the intended natural-language safety requirements.
    Ground-truth constraints are generated from these templates, so evaluation cannot detect hazards outside the template library.
  • ad hoc to paper A finite set of sampled execution trajectories can stand for the branching behavior of the agent for CTL verification.
    Section 3.3 samples five trajectories per task; the CTL universal quantifier is then applied only to these observed branches, not to all possible outcomes.
  • domain assumption LLM-generated high-level plans can be treated as finite traces over the same atomic propositions and time steps used in the LTL formulas.
    Plan-level checking in Algorithm 4 assumes a clean mapping from subgoal text to trace states; the paper gives no formal translation for this step.

pith-pipeline@v1.3.0-alltime-deepseek · 25872 in / 9821 out tokens · 83143 ms · 2026-08-04T09:48:46.447104+00:00 · methodology

0 comments
read the original abstract

We present SENTINEL, a framework for formally evaluating the physical safety of foundation model (FM)-based embodied agents. SENTINEL is the first to provide multi-level safety evaluation across semantic interpretation, plan generation, and physical execution within a unified formal framework. Unlike prior methods that rely on heuristic rules or subjective FM judgments, SENTINEL grounds practical safety requirements in formal temporal logic (TL) semantics that can precisely specify state invariants, temporal dependencies, and timing constraints. It employs a multi-level verification pipeline where (i) at the semantic level, intuitive natural language safety requirements are formalized into TL formulas and the agent's understanding of these requirements is probed for alignment with the TL formulas; (ii) at the plan level, high-level action plans and subgoals generated by the agent are verified against the TL formulas to detect unsafe plans before execution; and (iii) at the trajectory level, multiple execution trajectories are merged into a computation tree and efficiently verified against physically-detailed TL specifications for a final safety check. We apply SENTINEL in VirtualHome and AI2-THOR, and formally evaluate multiple FM-based embodied agents against diverse safety requirements. Our experiments show that by grounding physical safety in temporal logic and applying verification methods across multiple levels, SENTINEL provides a rigorous foundation for systematically evaluating the safety of FM-based embodied agents in simulation-based physical environments, and can effectively expose potential safety violations in interpreting, planning, and executing the tasks.

Figures

Figures reproduced from arXiv: 2510.12985 by Frank Yang, Huajie Shao, Kangrui Wang, Manling Li, Philip Wang, Qineng Wang, Qi Zhu, Ruohan Zhang, Simon Sinong Zhan, Xiangyu Shi, Xinyu Cao, Yao Liu, Yiyan Peng, Zhenyang Ni, Zhian Ruan, Zinan Wang.

Figure 1
Figure 1. Figure 1: Multi-level, progressive formal safety evaluation pipeline of [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Pipeline overview of Semantic-level safety checking and downstream plan generation. We ground natural language safety constraints into an LTL semantics, applying it to high-level plan generation for Theorem 2.2 with extensive constraints. Red highlights indicate the impact of enforcing safety constraints during plan generation. translation, we curate a set of ground-truth constraints Φ, and instantiate usi… view at source ↗
Figure 3
Figure 3. Figure 3: An illustrative walkthrough of trajectory safety evaluation of Theorem [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Correlation analysis between se￾mantic safety interpretation and plan-level safety. Across nearly all models, adding safety prompts improves performance: both natural language (NL) and LTL prompts yield higher Safe and Succ.&Safe scores compared to no safety prompt. This improvement shows that informing safety in both forms can nudge models toward safer behaviors. While NL prompts already provide benefits,… view at source ↗
Figure 5
Figure 5. Figure 5: Some examples of detailed physical safety violations, which can only be evaluated at trajectory [PITH_FULL_IMAGE:figures/full_fig_p009_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Pipeline from constraints generation to high-level plan generation. [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Modified ALFRED Scenes Breakdown Agent Evaluation. Following the VirtualHome protocol, we evaluate LLM agents in a zero-shot setting with prompts that encode ALFRED’s movement and planning rules. At initialization, the agent is provided with a detailed object list containing each object’s coordinate location and properties like whether the object is opened or closed. With complete object information of the… view at source ↗
Figure 8
Figure 8. Figure 8: Prompt for Safety Interpretation task. 18 [PITH_FULL_IMAGE:figures/full_fig_p018_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: System prompt for subgoals generation. 19 [PITH_FULL_IMAGE:figures/full_fig_p019_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Task specific prompt for subgoals generation. Noted the safety here can be either natural language [PITH_FULL_IMAGE:figures/full_fig_p020_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Task specific prompt for action generation. Noted the safety here can be either natural language [PITH_FULL_IMAGE:figures/full_fig_p021_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: Task specific prompt for action sequence generation. [PITH_FULL_IMAGE:figures/full_fig_p022_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: Toy problem to demonstrate CTL evaluation logic – robot to cut an apple in VirtualHome [PITH_FULL_IMAGE:figures/full_fig_p026_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: (a) Performance of four large LLMs on state invariance constraints, broken down by specific [PITH_FULL_IMAGE:figures/full_fig_p029_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Trajectory Safety Violation Analysis in a Cool and Place Task [PITH_FULL_IMAGE:figures/full_fig_p030_15.png] view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 4 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. SafeManip: A Property-Driven Benchmark for Temporal Safety Evaluation in Robotic Manipulation

    cs.RO 2026-05 unverdicted novelty 8.0

    SafeManip is a new benchmark that applies LTLf monitors to assess temporal safety properties across eight categories in robotic manipulation, demonstrating that task success frequently fails to ensure safe execution i...

  2. CreFlow: Corrective Reflow for Sparse-Reward Embodied Video Diffusion RL

    cs.CV 2026-05 conditional novelty 7.0

    CreFlow combines LTL compositional rewards with credit-aware NFT and corrective reflow losses in online RL to improve embodied video diffusion models, raising downstream task success by 23.8 percentage points on eight...

  3. SafeManip: A Property-Driven Benchmark for Temporal Safety Evaluation in Robotic Manipulation

    cs.RO 2026-05 unverdicted novelty 7.0

    SafeManip is a benchmark applying reusable LTLf templates across eight safety categories to evaluate temporal properties in robotic manipulation on VLA policies.

  4. STEP-LLM: Generating CAD STEP Models from Natural Language with Large Language Models

    cs.AI 2026-01 conditional novelty 6.0

    STEP-LLM fine-tunes LLMs to emit complete STEP CAD files from natural-language captions, reporting lower median Chamfer distance than Text2CAD.

Reference graph

Works this paper leans on

49 extracted references · 1 canonical work pages · cited by 3 Pith papers

  1. [1]

    write newline

    " write newline "" before.all 'output.state := FUNCTION n.dashify 't := "" t empty not t #1 #1 substring "-" = t #1 #2 substring "--" = not "--" * t #2 global.max substring 't := t #1 #1 substring "-" = "-" * t #2 global.max substring 't := while if t #1 #1 substring * t #2 global.max substring 't := if while FUNCTION format.date year duplicate empty "emp...

  2. [2]

    Achiam, D

    J. Achiam, D. Held, A. Tamar, and P. Abbeel. Constrained policy optimization. In Proceedings of the 34th International Conference on Machine Learning, volume 70 of ICML, pages 22--31, 2017

    2017

  3. [3]

    Alshiekh, R

    M. Alshiekh, R. Bloem, R. Ehlers, B. K \"o nighofer, S. Niekum, and U. Topcu. Safe reinforcement learning via shielding. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 32, 2018

    2018

  4. [4]

    G. Authors. Genesis: A generative and universal physics engine for robotics and beyond, December 2024. URL https://github.com/Genesis-Embodied-AI/Genesis

    2024

  5. [5]

    Baier and J.-P

    C. Baier and J.-P. Katoen. Principles of model checking. MIT press, 2008

    2008

  6. [6]

    P. Chao, E. Debenedetti, A. Robey, M. Andriushchenko, F. Croce, V. Sehwag, E. Dobriban, N. Flammarion, G. J. Pappas, F. Tramer, et al. Jailbreakbench: An open robustness benchmark for jailbreaking large language models. Advances in Neural Information Processing Systems, 37: 0 55005--55029, 2024

    2024

  7. [7]

    Y. Chen, J. Arkin, C. Dawson, Y. Zhang, N. Roy, and C. Fan. Autotamp: Autoregressive task and motion planning with llms as translators and checkers. In 2024 IEEE International conference on robotics and automation (ICRA), pages 6695--6702. IEEE, 2024 a

    2024

  8. [8]

    Z. Chen, F. Pinto, M. Pan, and B. Li. SafeWatch : An efficient safety-policy following video guardrail model with transparent explanations. arXiv:2412.06878, 2024 b

    Pith/arXiv arXiv 2024

  9. [9]

    Z. Chen, M. Kang, and B. Li. ShieldAgent : Shielding agents via verifiable safety policy reasoning. arXiv:2503.22738, 2025. doi:10.48550/arXiv.2503.22738

    doi:10.48550/arxiv.2503.22738 2025

  10. [10]

    E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on logic of programs, pages 52--71. Springer, 1981

    1981

  11. [11]

    Dawson, S

    C. Dawson, S. Gao, and C. Fan. Safe control with learned certificates: A survey of neural lyapunov, barrier, and contraction methods for robotics and control. IEEE Transactions on Robotics, 39 0 (3): 0 1749--1767, 2023

    2023

  12. [12]

    Desai, T

    A. Desai, T. Dreossi, and S. A. Seshia. Combining model checking and runtime verification for safe robotics. In International Conference on Runtime Verification, pages 172--189. Springer, 2017

    2017

  13. [13]

    Duret-Lutz, E

    A. Duret-Lutz, E. Renault, M. Colange, F. Renkin, A. Gbaguidi Aisse, P. Schlehuber-Caissier, T. Medioni, A. Martin, J. Dubois, C. Gillard, et al. From spot 2.0 to spot 2.10: What’s new? In International Conference on Computer Aided Verification, pages 174--187. Springer, 2022

    2022

  14. [14]

    D. J. Fremont, T. Dreossi, S. Ghosh, X. Yue, A. L. Sangiovanni-Vincentelli, and S. A. Seshia. Scenic: a language for scenario specification and scene generation. In Proceedings of the 40th ACM SIGPLAN conference on programming language design and implementation, pages 63--78, 2019

    2019

  15. [15]

    D. J. Fremont, E. Kim, Y. V. Pant, S. A. Seshia, A. Acharya, X. Bruso, P. Wells, S. Lemke, Q. Lu, and S. Mehta. Formal scenario-based testing of autonomous vehicles: From simulation to the real world. In 2020 IEEE 23rd International Conference on Intelligent Transportation Systems (ITSC), pages 1--8. IEEE, 2020

    2020

  16. [16]

    Fuggitti and T

    F. Fuggitti and T. Chakraborti. Nl2ltl--a python package for converting natural language (nl) instructions to linear temporal logic (ltl) formulas. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 37, pages 16428--16430, 2023

    2023

  17. [17]

    Hensel, S

    C. Hensel, S. Junges, J.-P. Katoen, T. Quatmann, and M. Volk. The probabilistic model checker storm. International Journal on Software Tools for Technology Transfer, 24 0 (4): 0 589--610, 2022

    2022

  18. [18]

    Howey, D

    R. Howey, D. Long, and M. Fox. VAL : Automatic plan validation, continuous effects and mixed-initiative planning using PDDL . In Proceedings of the 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI), 2004. doi:10.1109/ICTAI.2004.120

    doi:10.1109/ictai.2004.120 2004

  19. [19]

    Klauck, M

    M. Klauck, M. Steinmetz, J. Hoffmann, and H. Hermanns. Bridging the gap between probabilistic model checking and probabilistic planning: Survey, compilations, and empirical comparison. Journal of Artificial Intelligence Research, 68: 0 247--310, 2020. doi:10.1613/jair.1.11595

    work page doi:10.1613/jair.1.11595 2020

  20. [20]

    Kolve, R

    E. Kolve, R. Mottaghi, W. Han, E. VanderBilt, L. Weihs, A. Herrasti, D. Gordon, Y. Zhu, A. Gupta, and A. Farhadi. AI2-THOR: An Interactive 3D Environment for Visual AI . arXiv, 2017

    2017

  21. [21]

    Kwiatkowska, G

    M. Kwiatkowska, G. Norman, and D. Parker. Prism: Probabilistic symbolic model checker. In International Conference on Modelling Techniques and Tools for Computer Performance Evaluation, pages 200--204. Springer, 2002

    2002

  22. [22]

    Lacerda, F

    B. Lacerda, F. Faruq, D. Parker, and N. Hawes. Probabilistic planning with formal performance guarantees for mobile service robots. The International Journal of Robotics Research, 38 0 (9): 0 1098--1123, 2019

    2019

  23. [23]

    K. G. Larsen, P. Pettersson, and W. Yi. Uppaal in a nutshell. International journal on software tools for technology transfer, 1 0 (1): 0 134--152, 1997

    1997

  24. [24]

    C. Li, R. Zhang, J. Wong, C. Gokmen, S. Srivastava, R. Mart \' n-Mart \' n, C. Wang, G. Levine, M. Lingelbach, J. Sun, et al. Behavior-1k: A benchmark for embodied ai with 1,000 everyday activities and realistic simulation. In Conference on Robot Learning, pages 80--93. PMLR, 2023

    2023

  25. [25]

    M. Li, S. Zhao, Q. Wang, K. Wang, Y. Zhou, S. Srivastava, C. Gokmen, T. Lee, E. L. Li, R. Zhang, et al. Embodied agent interface: Benchmarking llms for embodied decision making. Advances in Neural Information Processing Systems, 37: 0 100428--100534, 2024

    2024

  26. [26]

    X. Lu, Z. Chen, X. Hu, Y. Zhou, W. Zhang, D. Liu, L. Sheng, and J. Shao. Is-bench: Evaluating interactive safety of vlm-driven embodied agents in daily household tasks. arXiv preprint arXiv:2506.16402, 2025

    arXiv 2025

  27. [27]

    Maler and D

    O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals. In International symposium on formal techniques in real-time and fault-tolerant systems, pages 152--166. Springer, 2004

    2004

  28. [28]

    A. Pnueli. The temporal logic of programs. In 18th annual symposium on foundations of computer science (sfcs 1977), pages 46--57. ieee, 1977

    1977

  29. [29]

    X. Puig, K. Ra, M. Boben, J. Li, T. Wang, S. Fidler, and A. Torralba. Virtualhome: Simulating household activities via programs. In Proceedings of the IEEE conference on computer vision and pattern recognition, pages 8494--8502, 2018

    2018

  30. [30]

    Savva, A

    M. Savva, A. Kadian, O. Maksymets, Y. Zhao, E. Wijmans, B. Jain, J. Straub, J. Liu, V. Koltun, J. Malik, et al. Habitat: A platform for embodied ai research. In Proceedings of the IEEE/CVF international conference on computer vision, pages 9339--9347, 2019

    2019

  31. [31]

    Shridhar, J

    M. Shridhar, J. Thomason, D. Gordon, Y. Bisk, W. Han, R. Mottaghi, L. Zettlemoyer, and D. Fox. Alfred: A benchmark for interpreting grounded instructions for everyday tasks. In Proceedings of the IEEE/CVF conference on computer vision and pattern recognition, pages 10740--10749, 2020

    2020

  32. [32]

    Tang, P.-Y

    Y.-C. Tang, P.-Y. Chen, and T.-Y. Ho. Defining and evaluating physical safety for large language models. arXiv:2411.02317, 2024

    Pith/arXiv arXiv 2024

  33. [33]

    M. Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for concurrency: structure versus automata, pages 238--266. Springer, 2005

    2005

  34. [34]

    C. Wang, C. Ross, Y.-L. Kuo, B. Katz, and A. Barbu. Learning a natural-language to ltl executable semantic parser for grounded robotics. In Conference on Robot Learning, pages 1706--1718. PMLR, 2021

    2021

  35. [35]

    Y. Wang, S. Zhan, Z. Wang, C. Huang, Z. Wang, Z. Yang, and Q. Zhu. Joint differentiable optimization and verification for certified reinforcement learning. In Proceedings of the ACM/IEEE 14th International Conference on Cyber-Physical Systems (with CPS-IoT Week 2023), pages 132--141, 2023 a

    2023

  36. [36]

    Y. Wang, S. S. Zhan, R. Jiao, Z. Wang, W. Jin, Z. Yang, Z. Wang, C. Huang, and Q. Zhu. Enforcing hard constraints with soft barriers: Safe reinforcement learning in unknown stochastic environments. In International Conference on Machine Learning, pages 36593--36604. PMLR, 2023 b

    2023

  37. [37]

    H. Wei, Z. Zhang, S. He, T. Xia, S. Pan, and F. Liu. Plangenllms: A modern survey of llm planning capabilities. arXiv preprint arXiv:2502.11221, 2025

    Pith/arXiv arXiv 2025

  38. [38]

    F. Yang, S. S. Zhan, Y. Wang, C. Huang, and Q. Zhu. Case study: runtime safety verification of neural network controlled system. In International Conference on Runtime Verification, pages 205--217. Springer, 2024

    2024

  39. [39]

    S. Yin, X. Pang, Y. Ding, M. Chen, Y. Bi, Y. Xiong, W. Huang, Z. Xiang, J. Shao, and S. Chen. Safeagentbench: A benchmark for safe task planning of embodied llm agents. arXiv preprint arXiv:2412.13178, 2024

    arXiv 2024

  40. [40]

    T. Yuan, Z. He, L. Dong, Y. Wang, R. Zhao, T. Xia, L. Xu, B. Zhou, F. Li, Z. Zhang, et al. R-judge: Benchmarking safety risk awareness for llm agents. arXiv preprint arXiv:2401.10019, 2024

    Pith/arXiv arXiv 2024

  41. [41]

    B. Zhan, X. Xu, Q. Gao, Z. Ji, X. Jin, S. Wang, and N. Zhan. Mars 2.0: A toolchain for modeling, analysis, verification and code generation of cyber-physical systems. arXiv preprint arXiv:2403.03035, 2024 a

    Pith/arXiv arXiv 2024

  42. [42]

    S. Zhan, Y. Wang, Q. Wu, R. Jiao, C. Huang, and Q. Zhu. State-wise safe reinforcement learning with pixel observations. In 6th Annual Learning for Dynamics & Control Conference, pages 1187--1201. PMLR, 2024 b

    2024

  43. [43]

    Zhang, H

    X. Zhang, H. Qin, F. Wang, Y. Dong, and J. Li. Lamma-p: Generalizable multi-agent long-horizon task allocation and planning with lm-driven pddl planner. arXiv preprint arXiv:2409.20560, 2024

    Pith/arXiv arXiv 2024

  44. [44]

    Q. Zhou, S. Chen, Y. Wang, H. Xu, W. Du, H. Zhang, Y. Du, J. B. Tenenbaum, and C. Gan. Hazard challenge: Embodied decision making in dynamically changing environments. arXiv preprint arXiv:2401.12975, 2024 a

    Pith/arXiv arXiv 2024

  45. [45]

    Y. Zhou, J. Yang, Y. Huang, K. Guo, Z. Emory, B. Ghosh, A. Bedar, S. Shekar, P.-Y. Chen, T. Gao, W. Geyer, N. Moniz, N. V. Chawla, and X. Zhang. LabSafety Bench : Benchmarking LLMs on safety issues in scientific labs. arXiv:2410.14182, 2024 b

    arXiv 2024

  46. [46]

    Z. Zhu, B. Wu, Z. Zhang, L. Han, Q. Liu, and B. Wu. Earbench: Towards evaluating physical risk awareness for task planning of foundation model-based embodied ai agents. arXiv preprint arXiv:2408.04449, 2024

    Pith/arXiv arXiv 2024

  47. [47]

    @esa (Ref

    \@ifxundefined[1] #1\@undefined \@firstoftwo \@secondoftwo \@ifnum[1] #1 \@firstoftwo \@secondoftwo \@ifx[1] #1 \@firstoftwo \@secondoftwo [2] @ #1 \@temptokena #2 #1 @ \@temptokena \@ifclassloaded agu2001 natbib The agu2001 class already includes natbib coding, so you should not add it explicitly Type <Return> for now, but then later remove the command n...

  48. [48]

    \@lbibitem[] @bibitem@first@sw\@secondoftwo \@lbibitem[#1]#2 \@extra@b@citeb \@ifundefined br@#2\@extra@b@citeb \@namedef br@#2 \@nameuse br@#2\@extra@b@citeb \@ifundefined b@#2\@extra@b@citeb @num @parse #2 @tmp #1 NAT@b@open@#2 NAT@b@shut@#2 \@ifnum @merge>\@ne @bibitem@first@sw \@firstoftwo \@ifundefined NAT@b*@#2 \@firstoftwo @num @NAT@ctr \@secondoft...

  49. [49]

    never place flammable objects near the stove

    @open @close @open @close and [1] URL: #1 \@ifundefined chapter * \@mkboth \@ifxundefined @sectionbib * \@mkboth * \@mkboth\@gobbletwo \@ifclassloaded amsart * \@ifclassloaded amsbook * \@ifxundefined @heading @heading NAT@ctr thebibliography [1] @ \@biblabel @NAT@ctr \@bibsetup #1 @NAT@ctr @ @openbib .11em \@plus.33em \@minus.07em 4000 4000 `\.\@m @bibit...

    arXiv