CoolFace
Apppublic

lukelike1001/behaverify-compositional

sourceHugging Faceupdated 5mo agoView on Hugging Face
0likes
App README

ACAS Xu A/G Contract Explorer

Interactive Gradio app for exploring Assume/Guarantee (A/G) contracts for the ACAS Xu closed-loop neuro-symbolic behavior tree, as described in:

Neuro-Symbolic Behavior Trees and Their Verification (NeuS 2025) Serbinowska et al. — https://proceedings.mlr.press/v288/serbinowska25a.html

What this app shows

Each A/G contract says: "From any dangerous state in input region R, neural network NN_k must NOT output advisory F." CROWN verifies this property over the entire input bounding box.

Panel layout:

1 — Original physical space2 — NN input space
3 — CROWN verification result4 — Contract metadata

Verification modes:

  • —Continuous (eps = 1e-4): one CROWN call over the full bounding box
  • —Discrete (eps = 0): one CROWN call per exact dangerous state

Set eps to 0 or 1e-4 to see the SAT/UNSAT bar chart in panel 3.

Data

Contracts cover NN1 (`aprev = clear`, 490 contracts) from the ACAS Xu closed-loop NSBT with a 10×10 integer grid state space and 40 headings.