PPAToolset

This repository provides infrastructure used for the experimental evaluation of the following publications:

Neural Network Action Policy Verification via Predicate Abstraction (tag: icaps22)

Neural Policy Safety Verification via Predicate Abstraction: CEGAR (tag: aaai23)

Neural Policy Safety Verification via Predicate Abstraction: Applicability Filtering (tag: icaps24)

The latest commit is tailored to the latest publications. Use the respective tags for earlier publications.

Code

Our approach is implemented on top of a PlaJA distribution and a modified Marabou version.

Further dependencies are:
nlohmann JSON library v3.11.2;
z3 (used z3-z3-4.8.12 and built with cmake -DCMAKE_BUILD_TYPE=Release -DZ3_SINGLE_THREADED=True);
Boost (used 1.81.0);
OpenBLAS-0.3.19;
Gurobi 9.5.1;
CxxTest 4.4 (only for Marabou's test infrastructure.).
Please see the code base README for proper pointers.

The code base is build with -DCMAKE_BUILD_TYPE=Release (we use version 3.27.1 and GCC/G++ (https://gcc.gnu.org/) version 12.3.1).
Paths to dependencies and build options must be set in CMakeLists.txt.
For ICPAS24 experiments configuration use:

SET(BUILD_PA ON) # PREDICATE ABSTRACTION

SET(ENABLE_APPLICABILITY_FILTERING ON)
SET(ENABLE_APPLICABILITY_CACHE ON)
SET(ENABLE_TERMINAL_STATE_SUPPORT ON)
SET(REACH_MAY_BE_TERMINAL OFF)
SET(MARABOU_DIS_BASELINE_SUPPORT ON)\

Benchmarks

The benchmarks can be found in the JANIBenchmarks repository.
The models/ subdirectory contains the benchmark instances, i.e., the automata networks.
The properties/ subdirectory contains the problem instances, i.e., a safety property and a neural action policy.
The networks/ subdirectory contains the neural networks -- referenced by the properties.

Running experiments

Base configuration:

${model} --additional-properties ${properties_file} --prop 1
--max-time 43200 --print-time 3600
--engine PA_CEGAR\

Applicability-filtering:
Enabled: --applicability-filtering 1
Disabled: --applicability-filtering -1 (default)

Reach-avoid:
Enabled: --set-pa-goal-objective-terminal true
Disabled: --set-pa-goal-objective-terminal false (default)

Per-Op-Disj:
Enabled: --per-op-app-dis true (default)
Disabled: --per-op-app-dis false

Opt-Slack-Var:
Enabled: --marabou-opt-slack-for-label-sel true --marabou-options "--opt-slack-for-dis 1 --opt-equality-in-dis 1" (default)
Disabled: --marabou-opt-slack-for-label-sel false --marabou-options "--opt-slack-for-dis 0 --opt-equality-in-dis 0"

Entail-Op:
Enabled: --cache-op-app cache-feasible --check-for-pa-terminal-states true (default)
Disabled: --cache-op-app none --check-for-pa-terminal-states false

Entail-Gen:
Enabled: --marabou-pre-opt-dis true --marabou-options "--pre-opt-dis 1 --advanced-entailment-ops-for-dis 1" (default)
Disabled: --marabou-pre-opt-dis false --marabou-options "--pre-opt-dis 0 --advanced-entailment-ops-for-dis 0"

--marabou-options must be concatenated.