Specifications¶

BehaVerify discharges three families of temporal-logic specifications through nuXmv: invariants, LTL, and CTL. Runtime monitors generated from LTL formulas additionally support contingency-triggered behaviors.

Invariants (`INVARSPEC`)¶

An INVARSPEC declares a state predicate that must hold in every reachable state.

specifications {
    INVARSPEC { (gte, battery_level, 0) }
    INVARSPEC { (and (gte, pos_x, 0) (lte, pos_x, x_max)) }
}

Invariants are the cheapest and most widely applicable family: nuXmv checks them by BDD-based reachability without any LTL/CTL overhead. Bounded history can be referenced via the at operator:

INVARSPEC { (implies (gt, (x at -1), 0) (gte, x, 0)) }

LTL (`LTLSPEC`)¶

An LTLSPEC quantifies over paths. BehaVerify’s prefix-notation temporal vocabulary:

Operator	Prefix form	Standard notation
next	`(next x)`	\(X\,\varphi\)
globally	`(globally x)`	\(G\,\varphi\)
finally	`(finally x)`	\(F\,\varphi\)
until	`(until x y)`	\(\varphi \, U \, \psi\)
release	`(release x y)`	\(\varphi \, R \, \psi\)

Example: battery monitor eventually triggers return-to-base when low.

LTLSPEC { (globally (implies (lt, battery_level, 20)
                             (finally at_home))) }

CTL (`CTLSPEC`)¶

Path-quantified temporal logic.

Operator	Prefix form	Standard notation
AG	`(always_globally x)`	\(A\,G\,\varphi\)
AF	`(always_finally x)`	\(A\,F\,\varphi\)
EG	`(exists_globally x)`	\(E\,G\,\varphi\)
EF	`(exists_finally x)`	\(E\,F\,\varphi\)

Example: a charging station is always eventually reachable.

CTLSPEC { (always_globally (exists_finally (eq, pos, charger))) }

Node-status atoms¶

Inside specifications only, four predicates are available that refer to the last-tick status of a named node:

(success node_name)
(failure node_name)
(running node_name)
(active node_name) – the node was evaluated on the last tick.

These are translated by BehaVerify into boolean expressions over the internal status encoding, so they compose naturally with the temporal operators above.

Contingency monitors¶

The monitors { ... } block attaches an LTL formula to an action that fires when the monitor becomes violated, turning a specification into runtime enforcement.

monitors {
    collision_monitor {
        specification LTLSPEC (globally (not collision_detected))
        trigger_action { emergency_stop }
    }
}

This emits three things:

An SMV constraint used by nuXmv to detect unreachable monitor states.
A compiled monitor class for the Python / C++ / Haskell runtimes.
A hook in the generated runner that calls the named trigger_action when the monitor fires.

See the “Verification of Behavior Trees with Contingency Monitors” paper (FMAS 2024) for the formal semantics.

Noisy environments¶

All four families above (INVAR, LTL, CTL, monitors) are handled by nuXmv. Stochasticity in the environment — a noisy sensor, a random action outcome — is encoded as non-deterministic choice, so the verifier proves the property against the worst case.