























Abstract:This paper presents a finite modal semantics where truth is closed under admissible continuation, then refined by discounted value, and finally certified by residual tests. The admissibility kernel is the classical greatest fixed point of a one-step predecessor expressing that some choice cell has all compatible successors inside a set. Certified choices are exactly local witnesses; the discounted value transformer is defined only over those witnesses; value-refined modal bisimulation is the coarsest local equivalence preserving formulas, kernel, certified choices, Bellman values, greedy sets, residual certificates, and public release certificates. A canonical pseudometric refines this equivalence: it is the unique fixed point of a Hausdorff-lifted choice-matching transformer over certified choices; its zero set is the value-refined bisimulation, and the optimal discounted value is one-Lipschitz with respect to it. Any approximate quotient incurs only a distance-bounded value error. Branching choice-cell and locus presentations place choice inside the model; the transition presentation is a conservative retraction. The same engine is applied to a public share-alike release fragment: attribution as label preservation, same-license propagation as derivative closure, no downstream restriction as admissibility, and the BY-SA witness as a residual-stable certificate. Finite examples show that altering the order of truth, admissibility, value, quotienting, public derivation, and certification changes the semantics.
From: Levent Sarioglu [view email]
[v1]
Fri, 5 Jun 2026 22:36:09 UTC (75 KB)
此内容由惯性聚合(RSS阅读器)自动聚合整理,仅供阅读参考。 原文来自 — 版权归原作者所有。