Pith. sign in

REVIEW 3 major objections 5 minor 36 references

Verification of Behavior Trees with Contingency Monitors

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

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

Pith's one-line read A Behavior Tree equipped with an LTL-derived contingency monitor can react to violations and be verified at design time.

desk verdict A solid workshop tool paper with an honest evaluation, but the design-time/runtime pipeline gap keeps the 'guaranteed' claim from being airtight. read the letter →

arxiv 2411.14162 v1 pith:XCNPH5Z7 submitted 2024-11-21 cs.RO

Serena S. Serbinowska , Nicholas Potteiger , Anne M. Tumlin , Taylor T. Johnson This is my paper · ORCID
classification cs.RO
keywords behaviortreesruntimemonitoringlineartemporallogicBuchiautomatacontingencymonitorsdesign-timeverificationnuXmvdronegrid-world
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

This paper claims that a Behavior Tree can be made self-correcting by attaching a contingency monitor derived automatically from a Linear Temporal Logic (LTL) specification. The monitor is generated by translating the LTL formula into a Buchi automaton, then implementing that automaton as a runtime check that reports whether the specification is violated, satisfied, or still undetermined. The paper also claims that the same monitor description can be turned into a nuXmv model, so the monitored tree can be verified before deployment, and that the generated monitors match the runtime performance of existing monitors while avoiding one correctness delay seen in the comparison tool. A sympathetic reader should care because behavior trees are widely used in robotics, and this gives a path from a temporal-logic requirement to a reactive, verifiable controller.

What carries the argument

The central object is the Behavior Tree with Monitor (BTM), defined as a tuple $(S,V,M,\Sigma_T,\Delta_M,s_0,v_0,m_0)$ in which the original BT state $S$, blackboard variables $V$, and environment inputs $\Sigma_T$ are joined by a monitor state set $M$, and the transition function $\Delta_M$ updates $S$, $V$, and $M$ together in response to each input. The carrying mechanism is the monitor itself: a Buchi automaton generated from the LTL specification by LTL2BA, implemented by tracking the set of possible automaton states after each step. The verdict logic is simple: no possible states means the specification is violated; a possible accepting state with a self-loop whose guard is always true means it is guaranteed; otherwise the verdict is unknown. This state-set construction is what lets the BT react to violations and be reset for repeated use, and the same specification is re-expressed in the BehaVerify DSL to create the nuXmv model used for design-time verification.

What would settle it

Run the same adversarial input trace through the generated Python or C monitor and through the nuXmv model of the same BTM and compare their verdicts at every step; any disagreement on a trace where the specification is violated or satisfied would show the design-time guarantee does not transfer to the runtime artifact.

Watch

Extended reading notes

Core claim

The central discovery is a complete pipeline from an LTL requirement to a Behavior Tree with a contingency monitor (BTM), together with evidence that the pipeline's runtime monitors are competitive and that the monitored tree can be design-time verified. Formally, the paper defines a BTM as a tuple extending a BT with a monitor state set and a transition function that updates tree, variables, and monitor together. Given an LTL formula, the tool creates a Buchi automaton via LTL2BA and implements it as a monitor that maintains the set of automaton states the trace could be in; an empty set means violation, an accepting self-loop with an always-true guard means the specification is guaranteed, and anything else is unknown. The tool also translates the same monitor into the BehaVerify DSL so nuXmv can prove that the BTM satisfies the specification, and that removing the monitor produces a counterexample. Benchmarks on a drone-grid scenario show the generated monitors are on par with Copilot in runtime, and the paper reports that its liveness monitor reports violations immediately whereas the Copilot monitor had a one-step delay.

Load-bearing premise

The design-time verification applies to a nuXmv model assembled from the DSL, while the runtime experiments run separately generated Python and C monitors, and the paper does not prove those representations behave identically.

Editorial extensions

If this is right

  • Users can specify a safety or liveness requirement in LTL and automatically obtain a monitor that plugs into a generated Python behavior tree and changes the tree's behavior when the requirement is about to be violated.
  • Design-time verification can show that the monitored tree satisfies the specification and produce a counterexample trace (a crash or a loop) if the monitor is removed, so the monitor's necessity is itself checkable.
  • The generated monitors are comparable to Copilot monitors in median runtime on the tested drone-grid scenarios, and the liveness monitor avoids the one-step delay reported for the comparison monitor.
  • Monitors can be swapped with little effort; the paper demonstrates mixing a Copilot safety monitor with a BehaVerify liveness monitor in the same tree.
  • Liveness verification remains expensive in nuXmv, but because the same liveness monitor is reused across grids, verifying it once on the smallest grid gives supporting evidence for the other instances.

Reading between the lines

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

  • The paper's guarantee would transfer to actual deployment only if the DSL model checked by nuXmv and the separately generated Python or C monitor are semantically equivalent; the paper does not establish that equivalence, so an adversarial trace that exercises a divergence would break the link between verification and runtime.
  • Because the monitor tracks the full set of possible Buchi states, the same construction should work for any LTL formula that LTL2BA can process, including richer conjunctions than the two tested grid specifications; a natural test is to benchmark against NuRV on harder formulas.
  • The reset mechanism suggests a design pattern in which a behavior tree re-arms a monitor after recovering, which matters for long-running missions where a single past violation should not permanently disable the contingency response.
  • Extending the same DSL pipeline to a C++ behavior-tree implementation would let the verified-monitor workflow reach a widely used industrial BT implementation, and such a port would be a stronger test of the claim that the monitors are tool-agnostic.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

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 introduces Behavior Trees with Monitors (BTMs), a formal extension of Behavior Trees in which an LTL runtime monitor can influence the tree's behavior via contingency actions. It extends the BehaVerify DSL to specify monitors, translates LTL specifications into Büchi automata with LTL2BA, and generates either Python/C monitor implementations for runtime or nuXmv models for design-time verification. The authors evaluate the runtime monitors on a grid-world drone navigation task, comparing them with NASA Copilot in terms of file size and median runtime, and report design-time verification results with nuXmv for safety and, partially, for liveness. The paper argues that the generated monitors are on par with Copilot and that the design-time verification can confirm the BTM satisfies its specifications.

Significance. The paper addresses an important gap in the behavior-tree ecosystem: connecting LTL requirements to runtime monitoring and design-time verification in a single toolchain. The open-source implementation and reproducible experiments are valuable, and the formal definition of BTM is a useful conceptual contribution. The comparison with Copilot is a concrete step toward establishing practical usability. However, the two major gaps identified below—semantic equivalence between the verified model and the runtime code, and lack of a correctness statement for the monitoring semantics—mean that the central claims currently outrun the evidence. If these gaps are closed, the toolchain would be a solid contribution to formal methods for autonomous systems.

major comments (3)
  1. [Section 4.5 and Section 6] The paper claims in Section 4.5 that the nuXmv pipeline is 'very similar' to the Python pipeline, but it provides no argument or proof that the monitor implementation in the generated .smv model is semantically equivalent to the Python/C monitor code that actually runs in the Section 5 experiments. The design-time verification results in Section 6 are therefore about an artifact different from the one evaluated at runtime. Because the BTM's contingency behavior depends on monitor verdicts, any divergence in the transition relation, reset conditions, or verdict encoding would invalidate the transfer of the verified safety or liveness property to the executed controller. The authors should either generate both artifacts from a common formal semantics with a correctness proof, verify the actual generated code, or at least demonstrate equivalence on the concrete examples (e.g., by co-simulation or equivalence checking).
  2. [Section 4.4] The monitoring algorithm's three-valued verdicts are described informally, and no correctness theorem is stated or proved. In particular, the 'guaranteed true' criterion (an accepting state with a self-loop with an always-true guard is reachable) is not a sound condition for the property to be true for all expected futures of the trace under nondeterministic BA semantics; the existence of an accepting run does not imply that all extensions satisfy the LTL formula. The reset behavior of the monitor is also not formally defined. Since the runtime reaction of the BTM is driven by these verdicts, the paper should state the intended monitoring semantics (e.g., soundness and completeness w.r.t. a defined subset of LTL) and prove that the algorithm implements it, or clearly delimit the fragment for which the verdicts are correct.
  3. [Section 5.4] The timing comparison subtracts the monitorless baseline from the monitored runs, but this is not a valid way to isolate monitor overhead because the presence of the monitor changes the drone's behavior: the whole point of the monitor is to trigger contingency actions, so the monitored and monitorless systems take different trajectories and may perform different numbers of ticks. The median difference between the monitored and monitorless runtimes therefore measures behavioral change plus monitor cost, not monitor cost alone. The claim that the generated monitors are 'on par' with Copilot is not established by these numbers. The authors should report total wall-clock times for the complete systems, or design a scenario where the behavioral paths are identical and only the monitor computation differs, or report the per-tick monitor cost separately.
minor comments (5)
  1. [Section 4.1] In the displayed equation defining the BTM trace, the transition function is written as ∆T but should be ∆M; the formal definition is otherwise inconsistent.
  2. [Section 5.3] The hardware description says '24 core 13th Gen Intel(R) Core(TM) i7-13700K', but the i7-13700K has 16 cores (24 threads); this should be corrected for reproducibility.
  3. [Section 5.1] The specifications φS and φL are described as safety and liveness, respectively, but the paper itself notes that both monitored formulas φS1 and φL1 are safety properties in the formal sense; the terminology should be clarified to avoid confusion.
  4. [Section 2] The claim that the method 'allows us to prove that a BT equipped with a monitor and its contingency response for detected violations is guaranteed to satisfy a specification' is too strong given that Section 6 reports liveness verification only for a single grid and safety verification only for a subset of the grids considered; the claim should be qualified to the actually verified instances.
  5. [Section 4.4] The paper states that the monitor 'can be reset' but does not precisely specify when or how the reset occurs in the DSL or in the generated code, which is relevant for the monitor's behavior over repeated runs.

Circularity Check

0 steps flagged · score 2.0 of 10

No significant circularity: monitors are generated from LTL2BA automata and checked against external Copilot and nuXmv; the main caveats are unverified translation equivalence, not circularity.

full rationale

No circular step reduces a claimed result to its inputs. The monitors are generated from LTL2BA, an external tool, from user-supplied LTL formulas, and the runtime comparison against NASA Copilot is an external benchmark. The nuXmv design-time verification checks reachability and liveness properties of the composed BTM model rather than assuming the monitor's verdicts: the monitor transition relation is constructed from the LTL2BA never-claim and used as a component, and the verified properties φS and φL are distinct from the monitored formulas φS1 and φL1. The paper's own caveats point to the actual weakness, which is a correctness gap rather than circularity: Section 4.5 says 'The nuXmv pipeline is very similar to the Python pipeline, and as such we will avoid going into the inner workings of this pipeline,' and Section 5.4 says 'While these example traces are not conclusive proof'. No formal semantic equivalence is established between the runtime Python/C monitors and the .smv model checked by nuXmv, so the design-time guarantee may not transfer to the executed artifact; Section 6 even describes the liveness verification as 'limited verification process' providing only 'some evidence'. These are transfer and evidence gaps, not reductions by construction. The self-citation to BehaVerify [27] is to the tool being extended, not to an authority that supplies the paper's correctness claims, so it is not load-bearing.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No numerical parameters are fitted; the central claim rests on the correctness of external tools (LTL2BA, nuXmv), the chosen monitor verdict semantics for finite prefixes, and the assumption that the generated nuXmv model faithfully represents the executed Python/C code.

assumptions (4)
  • domain assumption LTL2BA correctly translates any LTL formula into a Buchi automaton recognizing exactly the satisfying traces.
    The monitor pipeline depends on LTL2BA's correctness; any translation bug directly corrupts the generated monitors. Invoked in Section 4.4.
  • ad hoc to paper The three-valued monitor verdicts (violation if no possible states, guaranteed true if an accepting self-loop with an always-true guard is reachable, unknown otherwise) correctly implement the desired LTL monitoring semantics for the formulas used.
    The monitor defines 'violation' and 'guaranteed true' based on the set of possible BA states and accepting self-loops; the paper does not prove this abstraction is sound and complete for arbitrary LTL formulas, only that it works on the examples. Section 4.4.
  • ad hoc to paper The nuXmv model generated from the BehaVerify DSL is semantically equivalent to the Python/C monitor code executed in the runtime experiments.
    Design-time verification conclusions are drawn from the nuXmv model while performance and correctness are measured on the generated code; equivalence is assumed, not proven. Sections 4.4, 4.5, 6.
  • domain assumption The formal BT semantics defined in Section 3.4 adequately captures the execution of the generated PyTrees code.
    The tool targets PyTrees, and the formal tuple is used for verification; the link between the formal semantics and the concrete implementation is not mechanically checked. Section 3.4 and 4.3.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Verification of Behavior Trees with Contingency Monitors." pith.science (2026). https://pith.science/paper/XCNPH5Z7

@misc{pith2026241114162,
  author       = {Pith},
  title        = {Pith review of: Verification of Behavior Trees with Contingency Monitors},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/XCNPH5Z7}},
  note         = {Machine review of arXiv:2411.14162}
}
read the original abstract

Behavior Trees (BTs) are high level controllers that have found use in a wide range of robotics tasks. As they grow in popularity and usage, it is crucial to ensure that the appropriate tools and methods are available for ensuring they work as intended. To that end, we created a new methodology by which to create Runtime Monitors for BTs. These monitors can be used by the BT to correct when undesirable behavior is detected and are capable of handling LTL specifications. We demonstrate that in terms of runtime, the generated monitors are on par with monitors generated by existing tools and highlight certain features that make our method more desirable in various situations. We note that our method allows for our monitors to be swapped out with alternate monitors with fairly minimal user effort. Finally, our method ties in with our existing tool, BehaVerify, allowing for the verification of BTs with monitors.

Figures

Figures reproduced from arXiv: 2411.14162 by the authors.

Figure 1
Figure 1. Example Leaf and Decorator Nodes. Node a Node d x :=x+2 S Node c (x≤2)?S:F Node b x :=x+1 S Tick 1 1 1 1 1 1 1 2 2 2 2 2 t 1 2 3 4 5 6 7 8 9 10 11 12 Active a b a c a d a a b a c a Returns - S - S - S S - S - F F x 0 1 1 1 1 3 3 3 4 4 4 4 [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. A BT consisting of a sequence node (a) with two actions (b, d) and a check (c). We use the ternary operator i? j : k to mean if i then j else k. Tick indicates the number of times the tree has been ticked. At each timestep t, the variable x is updated based on the active node. If a node is finished, then it returns one of S, F, or R. Decorator Nodes Decorator nodes ‘decorate’ their children, allowing for easy adjust… view at source ↗
Figure 3
Figure 3. Diagram of how BehaVerify generates Python code for BTs with mon￾itors. LTL2BA is a tool for converting an LTL specification to a BA. Spin is a model checker, and a Never Claim can be checked using Spin. Solid blue arrows mark new contributions. 4.4 Generating Implementations We utilize the following process to generate a BT M using BehaVerify. 1. The user creates a DSL file specifying the BT and any monitors it use… view at source ↗
Figures from the paper (5 more)
Figure 5
Figure 5. Figure 5: Images representing some of the grids used for the scaling experiments. The upper grids are [PITH_FULL_IMAGE:figures/full_fig_p010_5.png]
Figure 6
Figure 6. Figure 6: Pictures are ordered left to right. The drone (blue) is trying to reach the destination (green) [PITH_FULL_IMAGE:figures/full_fig_p011_6.png]
Figure 7
Figure 7. Figure 7: A screenshot of the drone flying in AirSim and a grid visualization. [PITH_FULL_IMAGE:figures/full_fig_p012_7.png]
Figure 8
Figure 8. Figure 8: Top left: file sizes of safety monitors for dense fixed. Top right: file sizes of safety monitors for [PITH_FULL_IMAGE:figures/full_fig_p013_8.png]
Figure 9
Figure 9. Figure 9: The graph shows the time (in seconds) to verify that the BT M is safe (does not crash into obstacles). The verification was done with nuXmv. Liveness specifications are considerably harder to verify, with the 9 by 9 sparse grid taking about 25 minutes to verify. As thi…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

36 extracted references · 8 canonical work pages

  1. [1]

    Available at https://www.behaviortree.dev/docs/tutorial -basics/tutorial_02_basic_ports

    Auryn Robotics: Tutorial 02: Blackboard and Ports. Available at https://www.behaviortree.dev/docs/tutorial -basics/tutorial_02_basic_ports

  2. [2]

    Chivukula, Olugbemiga Adekunle, Mu Sun, Marco Caccamo & Lui Sha (2009): The System-Level Simplex Architecture for Improved Real-Time Embedded System Safety

    Stanley Bak, Deepti K. Chivukula, Olugbemiga Adekunle, Mu Sun, Marco Caccamo & Lui Sha (2009): The System-Level Simplex Architecture for Improved Real-Time Embedded System Safety. In: 2009 15th IEEE Real-Time and Embedded Technology and Applications Symposium, pp. 99–107, doi:10.1109/RTAS.2009.20

    work page doi:10.1109/rtas.2009.20 2009

  3. [3]

    ACM Trans

    Andreas Bauer, Martin Leucker & Christian Schallhart (2011): Runtime Verification for LTL and TLTL. ACM Trans. Softw. Eng. Methodol. 20(4), doi:10.1145/2000799.2000800

    arXiv 2011

  4. [4]

    IEEE Robotics and Automation Letters 5(2), pp

    Oliver Biggar & Mohammad Zamani (2020): A Framework for Formal Verification of Behavior Trees With Linear Temporal Logic . IEEE Robotics and Automation Letters 5(2), pp. 2341–2348, doi:10.1109/LRA.2020.2970634

    arXiv 2020

  5. [5]

    IEEE Robotics and Automation Letters 6(3), pp

    Oliver Biggar, Mohammad Zamani & Iman Shames (2021): An Expressiveness Hierarchy of Behav- ior Trees and Related Architectures . IEEE Robotics and Automation Letters 6(3), pp. 5397–5404, doi:10.1109/lra.2021.3074337

    arXiv 2021

  6. [6]

    In: CA V, pp

    Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri & Stefano Tonetta (2014):The nuXmv Symbolic Model Checker. In: CA V, pp. 334–342. Available at http://dx.doi.org/10.1007/978-3-319-08867-9_22

    doi:10.1007/978-3-319-08867-9_22 2014

  7. [7]

    In Bernd Finkbeiner & Leonardo Mariani, editors: Runtime Verification, Springer International Publishing, Cham, pp

    Alessandro Cimatti, Chun Tian & Stefano Tonetta (2019): NuRV: A nuXmv Extension for Runtime Verification. In Bernd Finkbeiner & Leonardo Mariani, editors: Runtime Verification, Springer International Publishing, Cham, pp. 382–392, doi:10.1007/978-3-030-32079-9_23

    work page doi:10.1007/978-3-030-32079-9_23 2019

  8. [8]

    Domenichelli, Lorenzo Natale & Armando Tacchella (2021): Formalizing the Execution Context of Behavior Trees for Runtime Verification of Deliberative Policies

    Michele Colledanchise, Giuseppe Cicala, Daniele E. Domenichelli, Lorenzo Natale & Armando Tacchella (2021): Formalizing the Execution Context of Behavior Trees for Runtime Verification of Deliberative Policies. In: 2021 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS) , IEEE Press, pp. 9841–9848, doi:10.1109/IROS51168.2021.9636129

    arXiv 2021

Show all 36 references
  1. [9]

    In: 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems, pp

    Michele Colledanchise & Petter Ögren (2014):How Behavior Trees modularize robustness and safety in hybrid systems. In: 2014 IEEE/RSJ International Conference on Intelligent Robots and Systems, pp. 1482–1488, doi:10.1109/IROS.2014.6942752. S. Serbinowska, N. Potteiger, A. Tumli...

    2014

  2. [10]

    In: 2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp

    Michele Colledanchise & Petter Ögren (2016): How Behavior Trees generalize the Teleo-Reactive paradigm and And-Or-Trees. In: 2016 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS), pp. 424–429, doi:10.1109/IROS.2016.7759089

    2016

  3. [11]

    IEEE Transactions on Robotics 33(2), pp

    Michele Colledanchise & Petter Ögren (2017): How Behavior Trees Modularize Hybrid Control Systems and Generalize Sequential Behavior Compositions, the Subsumption Architecture, and Decision Trees. IEEE Transactions on Robotics 33(2), pp. 372–389, doi:10.1109/TRO.2016.2633567

    2017

  4. [12]

    In Christian Colombo & Martin Leucker, editors: Runtime Verification, Springer International Publishing, Cham, pp

    Antoine El-Hokayem & Yliès Falcone (2018): Bringing Runtime Verification Home. In Christian Colombo & Martin Leucker, editors: Runtime Verification, Springer International Publishing, Cham, pp. 222–240, doi:10.1007/978-3-030-03769-7_13

    2018 doi

  5. [13]

    Available at https://docs.unrealengine.com/4.27/en-US/Interactiv eExperiences/\ArtificialIntelligence/BehaviorTrees/BehaviorTreesOverview/

    EpicGames (2021): Behavior tree overview. Available at https://docs.unrealengine.com/4.27/en-US/Interactiv eExperiences/\ArtificialIntelligence/BehaviorTrees/BehaviorTreesOverview/

    2021

  6. [14]

    Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini & Viviana Mascardi (2020): ROSMonitoring: A Runtime Verification Framework for ROS

    Angelo Ferrando, Rafael C. Cardoso, Michael Fisher, Davide Ancona, Luca Franceschini & Viviana Mascardi (2020): ROSMonitoring: A Runtime Verification Framework for ROS. In Abdelkhalick Mohammad, Xin Dong & Matteo Russo, editors: Towards Autonomous Robotic Systems, Springer Int...

    2020 doi

  7. [15]

    Angelo Ferrando & Vadim Malvone (2022): Towards the Combination of Model Checking and Runtime Verification on Multi-agent Systems. In Frank Dignum, Philippe Mathieu, Juan Manuel Corchado & Fer- nando De La Prieta, editors: Advances in Practical Applications of Agents, Multi-Ag...

    2022 doi

  8. [16]

    In Gérard Berry, Hubert Comon & Alain Finkel, editors: Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, pp

    Paul Gastin & Denis Oddoux (2001): Fast LTL to Büchi Automata Translation. In Gérard Berry, Hubert Comon & Alain Finkel, editors: Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 53–65, doi:10.1007/3-540-44585-4_6

    2001 doi

  9. [17]

    In Jan Friso Groote & Kim Guldstrand Larsen, editors: Tools and Algorithms for the Construction and Analysis of Systems, Springer International Publishing, Cham, pp

    Felipe Gorostiaga & César Sánchez (2021): HLola: a Very Functional Tool for Extensible Stream Runtime Verification. In Jan Friso Groote & Kim Guldstrand Larsen, editors: Tools and Algorithms for the Construction and Analysis of Systems, Springer International Publishing, Cham,...

    2021 doi

  10. [18]

    In: 2022 International Conference on Robotics and Automation (ICRA), pp

    Zhaoyuan Gu, Nathan Boyd & Ye Zhao (2022): Reactive Locomotion Decision-Making and Robust Motion Planning for Real-Time Perturbation Recovery. In: 2022 International Conference on Robotics and Automation (ICRA), pp. 1896–1902, doi:10.1109/ICRA46639.2022.9812068

    2022

  11. [19]

    In Jan Friso Groote & Marieke Huisman, editors: Formal Methods for Industrial Critical Systems, Springer International Publishing, Cham, pp

    Thomas Henn, Marcus Völker, Stefan Kowalewski, Minh Trinh, Oliver Petrovic & Christian Brecher (2022): Verification of Behavior Trees using Linear Constrained Horn Clauses . In Jan Friso Groote & Marieke Huisman, editors: Formal Methods for Industrial Critical Systems, Springe...

    2022 doi

  12. [20]

    Holzmann (1997): The model checker SPIN

    G.J. Holzmann (1997): The model checker SPIN. IEEE Transactions on Software Engineering 23(5), pp. 279–295, doi:10.1109/32.588521

    1997 doi

  13. [21]

    Robotics and Autonomous Systems 154, p

    Matteo Iovino, Edvards Scukins, Jonathan Styrud, Petter Ögren & Christian Smith (2022):A survey of Behavior Trees in robotics and AI. Robotics and Autonomous Systems 154, p. 104096, doi:10.1016/j.robot.2022.104096

    2022

  14. [22]

    In: 2014 IEEE International Conference on Robotics and Automation (ICRA), pp

    Alejandro Marzinotto, Michele Colledanchise, Christian Smith & Petter Ögren (2014): Towards a unified behavior trees framework for robot control . In: 2014 IEEE International Conference on Robotics and Automation (ICRA), pp. 5420–5427, doi:10.1109/ICRA.2014.6907656

    2014

  15. [23]

    Available at https://move4bt.github.io/

    Huang Peishan, Hong Weijiang, Chen Zhenbang & Wang Ji: MoVe4BT: Modeling & Verification For BT. Available at https://move4bt.github.io/. Accessed: 2023-12-14

    2023

  16. [24]

    Technical Report Technical Report NASA/TM- 2020-220587, NASA

    Ivan Perez, Frank Dedden & Alwyn Goodloe (2020):Copilot 3. Technical Report Technical Report NASA/TM- 2020-220587, NASA

    2020

  17. [25]

    Ivan Perez, Anastasia Mavridou, Tom Pressburger, Alwyn Goodloe & Dimitra Giannakopoulou (2022): Automated Translation of Natural Language Requirements to Runtime Monitors. In Dana Fisman & Grigore 72 Verification of BT with Monitors Rosu, editors: Tools and Algorithms for the ...

    2022 doi

  18. [26]

    IEEE Transactions on Cybernetics53(8), pp

    Fangbo Qin, De Xu, Blake Hannaford & Tiantian Hao (2023): Object-Agnostic Vision Measurement Frame- work Based on One-Shot Learning and Behavior Tree. IEEE Transactions on Cybernetics53(8), pp. 5202–5215, doi:10.1109/TCYB.2022.3181054

    2023

  19. [27]

    Serbinowska & Taylor T

    Serena S. Serbinowska & Taylor T. Johnson (2022): BehaVerify: Verifying Temporal Logic Specifications For Behavior Trees. In: Software Engineering and Formal Methods: 20th International Conference, SEFM 2022, Berlin, Germany, September 26-30, 2022, Proceedings, Springer-Verlag...

    2022 doi

  20. [28]

    D. Seto, B. Krogh, L. Sha & A. Chutinan (1998): The Simplex architecture for safe online control system upgrades. In: Proceedings of the 1998 American Control Conference. ACC (IEEE Cat. No.98CH36207), 6, pp. 3504–3508 vol.6, doi:10.1109/ACC.1998.703255

    1998

  21. [29]

    Seto & L

    D. Seto & L. Sha (1999): A Case Study on Analytical Analysis of the Inverted Pendulum Real-Time Control System. Technical Report, DTIC and NTIS. 10.21236/ADA373286

    1999 doi

  22. [30]

    In Marco Hutter & Roland Siegwart, editors: Field and Service Robotics, Springer International Publishing, Cham, pp

    Shital Shah, Debadeepta Dey, Chris Lovett & Ashish Kapoor (2018): AirSim: High-Fidelity Visual and Physical Simulation for Autonomous Vehicles. In Marco Hutter & Roland Siegwart, editors: Field and Service Robotics, Springer International Publishing, Cham, pp. 621–635, doi:10....

    2018 doi

  23. [31]

    Sprague & Petter Ögren (2022): Continuous-Time Behavior Trees as Discontinuous Dynamical Systems

    Christopher I. Sprague & Petter Ögren (2022): Continuous-Time Behavior Trees as Discontinuous Dynamical Systems. IEEE Control Systems Letters 6, pp. 1891–1896, doi:10.1109/LCSYS.2021.3134453

    2022

  24. [32]

    Available at https://py-trees.readthedocs.io/en/devel/modules.html

    Daniel Stonier: PyTrees Module API. Available at https://py-trees.readthedocs.io/en/devel/modules.html. Accessed: 2023-12-14

    2023

  25. [33]

    In: 2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks - Supplemental V olume (DSN-S), pp

    Alexander Will, Aidan Collins, Robert Grizzard, Smitha Gautham, Patrick Martin, Evan Dill & Carl Elks (2023): An Integrated Runtime Verification and Simulation Testbed for UAM Hazard Assessment. In: 2023 53rd Annual IEEE/IFIP International Conference on Dependable Systems and ...

    2023

  26. [34]

    In: 2021 IEEE International Conference on Robotics and Automation (ICRA) , pp

    Sebastián Zudaire, Felipe Gorostiaga, César Sánchez, Gerardo Schneider & Sebastián Uchitel (2021): Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Execu- tions. In: 2021 IEEE International Conference on Robotics and Automation (ICRA) , pp. 6824–6830...

    2021

  27. [35]

    IEEE Robotics and Automation Letters 5(4), pp

    Petter Ögren (2020): Convergence Analysis of Hybrid Control Systems in the Form of Backward Chained Behavior Trees. IEEE Robotics and Automation Letters 5(4), pp. 6073–6080, doi:10.1109/LRA.2020.3010747

    2020

  28. [36]

    Sprague (2022): Behavior Trees in Robot Control Systems

    Petter Ögren & Christopher I. Sprague (2022): Behavior Trees in Robot Control Systems. Annual Review of Control, Robotics, and Autonomous Systems 5(V olume 5, 2022), pp. 81–107, doi:10.1146/annurev-control- 042920-095314

    2022 doi

Pith tools

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