发表机构
Universidad Torcuato Di Tella（托卡托迪特拉大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对有限状态模型，提出综合最小充分观察契约的方法，通过穷举或SAT/MaxSAT编码实现基数或成本目标下的精确综合，并验证充分性，实验表明方法高效且有效。
AI 中文摘要
我们将本文推导并验证的对象称为最小充分治理上下文：给定一个有限可达状态模型、一个确定性的声明判定以及候选可观察属性，我们计算充分的观察集，区分单独不可或缺的属性与联合充分的契约，并在基数或声明成本目标下从充分契约中进行选择。观察契约是一组候选属性，其值在每个可达状态上决定声明判定；权威契约是在目标下选择并绑定到门模式的契约。在穷举枚举可行的情况下，我们综合所有包含最小充分契约，否则通过SAT/MaxSAT编码综合最小基数或最小成本契约，并直接检查充分性。在一个构造的代码/云领域，单独不可或缺的核心作为观察契约并不充分，且存在两个不同的约简；一个预注册的成本模型精确地区分了它们。在第二个更大的构造领域中，相同的模式重现，但该领域的成本模型未能区分备选方案：一个完全解释的成本平局，被报告为已发现。我们测量了可分辨性族的规模，在注册超时内确认穷举枚举不可行，而SAT/MaxSAT综合在远低于一秒内解决；MaxSAT未显示出比普通SAT更大的基数优势。AuthorityBench在三个领域上比较了四个基线；仅声明基线在任何领域上都不精确充分。每个选定的契约都检查充分性，失败时提供反例，成功时提供检查摘要而非可移植证书——这是两范围表中以编译器为重点的范围；一个独立指定的端到端案例研究是注册的后续工作，此处不声称。
英文摘要
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.
CommentsCode, data, preregistration tags, review record, and independent reproduction (repository issue #3): https://github.com/besanson/sarc-authority-derivation. Artifact DOI: 10.5281/zenodo.22884173
