Theory¶
What behavior trees are, how BehaVerify translates them into SMV, how nuXmv discharges the resulting specifications, and why the end-to-end result is trustworthy.
All content on these pages is grounded in the four BehaVerify papers
(see Publications) and in the code under
src/behaverify/.
Node taxonomy, operational semantics, and the tick relation.
Invariants, LTL, CTL — syntax, semantics, and expressiveness.
The fast-forwarding encoding and its variable-staging scheme.
BDDs, bounded model checking, IC3 / PDR; what each algorithm decides.
End-to-end argument: why a verified property on the SMV model implies the same property on the BT.
How ONNX leaves are compiled into SMV without changing the tick semantics.
Node-local state that persists across ticks (FMAS 2024).
LTL safety monitors with trigger actions (FMAS 2024).