Summary
Some computer systems need to decide if certain rules are followed by looking at specific signals or data points, but not all data is useful or needed for making those decisions. This paper shows how to find the smallest and most cost-effective sets of observations that still allow the system to know the correct verdict on every possible state. The authors use logical methods to confirm which observations are essential alone and which groups work together to make decisions. Their method helps choose the best sets based on size or cost, tested on example scenarios where their approach quickly finds solutions.
What this means in practice
- •For cloud security teams: Identify minimal sets of log attributes to monitor that guarantee exact detection of policy violations in complex cloud systems.
- •For software testers: Optimize test instrumentation by selecting smallest attribute sets ensuring conclusive verdicts for code behavior correctness.
Abstract
We call the object this paper derives and certifies a minimal sufficient governance context: given a finite reachable-state model, a deterministic declared verdict, and candidate observable attributes, we compute sufficient observation sets, distinguish attributes that are individually indispensable from contracts that are jointly sufficient, and select among sufficient contracts under a cardinality or declared-cost objective. An observation contract is a set of candidate attributes whose values determine the declared verdict on every reachable state; an authority contract is one selected under an objective and bound to a gate schema. We synthesize every inclusion-minimal sufficient contract where exhaustive enumeration is affordable, and a minimum-cardinality or minimum-cost contract by SAT/MaxSAT encoding otherwise, checking sufficiency directly. On a constructed code/cloud domain, the individually-indispensable core is not sufficient as an observation contract and two distinct reducts exist; a preregistered cost model separates them exactly. On a second, larger, constructed domain, the same pattern recurs, but that domain's cost model does not separate the alternatives: a fully explained cost tie, reported as found. We measure discernibility-family scaling where exhaustive enumeration is confirmed infeasible within a registered timeout, while SAT/MaxSAT synthesis solves in well under a second; MaxSAT showed no measured cardinality advantage over plain SAT. AuthorityBench compares four baselines across three domains; the declared-only baseline is not exactly sufficient on any. Every selected contract is checked for sufficiency, with a counterexample on failure and a check summary, not a portable certificate, on success -- the compiler-focused scope of a two-scope table; an independently specified end-to-end case study is registered follow-up work, not claimed here.