Glossary

BT

Behavior tree. A rooted tree whose internal nodes are control flow (sequence, selector, parallel) and whose leaves are conditions and actions.

BT.CPP

BehaviorTree.CPP, a widely used C++ implementation of behavior trees for ROS 2 and other robotics stacks.

blackboard

Shared mutable state accessible to every tree node. Declared with the bl scope tag.

CTL

Computation Tree Logic. Path-quantified temporal logic.

fast-forwarding encoding

BehaVerify’s default SMV encoding where one behavior-tree tick becomes one SMV transition. See Encodings.

INVARSPEC

An nuXmv invariant specification: a predicate that must hold in every reachable state.

leaf node

A behavior-tree node with no children — either a check or an action.

LTL

Linear Temporal Logic.

monitor

An LTL formula compiled to a runtime automaton that fires a trigger action when violated.

nuXmv

nuXmv, a symbolic model-checker used by BehaVerify for formal verification.

ONNX

Open Neural Network Exchange format; the representation BehaVerify uses for neural leaves.