http://w3id.org/dpp/access-control/asp · Version 1.0.0
A design-time formal-verification layer for the dpp-ac access-control policy set. The encoding is a faithful bounded abstraction of the runtime SPARQL decision pipeline (rules R01 to R10 over the OWL 2 DL and SHACL model), evaluated with the clingo answer-set solver. It checks, over the whole policy space at once, properties that per-request evaluation cannot establish exhaustively.
The abstraction mirrors only the decision-relevant rules (R01, R02, R06, R07, R08, R09). The temporal and purpose rules (R03, R04) are provenance markers that do not gate the decision, and R05 duplicates the gate already in R01. The six built-environment scenarios are reproduced exactly (four grants, two denials) as a faithfulness gate before any property is asserted.
| Property | Meaning |
|---|---|
| P1 Conflict-freeness | No combination is both permitted and prohibited. |
| P2 Determinism and totality | Every combination receives exactly one outcome. |
| P3 Role and policy coverage | Reproduces the SPARQL role-coverage result. |
| P4 Exhaustive enumeration | The full role by action by category decision surface. |
pip install clingo python run_verification.py
The program is deterministic, so it yields a single stable model and the same report on every run. The saved report is linked above.