pith. sign in

arxiv: 2606.07884 · v1 · pith:TH6LMAOMnew · submitted 2026-06-05 · 💻 cs.LO

Value-Refined Modal Fixed-Point Semantics with Certified Choice and Public Share-Alike Certificates

Faruk Alpay , Levent Sarioglu This is my paper

Pith reviewed 2026-06-27 19:58 UTC · model grok-4.3

classification 💻 cs.LO
keywords modal logicfixed-point semanticsbisimulationdiscounted valueadmissibility kernelcertified choicespseudometricpublic certificates
0
0 comments X

The pith

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 machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents a finite modal semantics in which truth is closed under admissible continuation, refined by discounted value, and certified by residual tests. The admissibility kernel is constructed as the greatest fixed point of a one-step predecessor over choice cells, and the discounted value transformer operates only on certified witnesses. Value-refined modal bisimulation is shown to be the coarsest local equivalence that preserves formulas, the kernel, certified choices, Bellman values, greedy sets, residual certificates, and public release certificates. A canonical pseudometric refines this equivalence as the unique fixed point of a Hausdorff-lifted transformer, ensuring the optimal discounted value is one-Lipschitz continuous and that approximate quotients have distance-bounded value errors. The approach is also applied to a public share-alike fragment with analogous preservation rules for attribution and licenses.

Core claim

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 while the transition presentation is a conservative retraction. The same engine is

What carries the argument

Value-refined modal bisimulation, the coarsest local equivalence preserving formulas, kernel, certified choices, Bellman values, greedy sets, residual certificates, and public release certificates

If this is right

  • The optimal discounted value is one-Lipschitz with respect to the canonical pseudometric.
  • Any approximate quotient incurs only a distance-bounded value error.
  • The transition presentation is a conservative retraction of the branching choice-cell and locus presentations.
  • The framework extends to a public share-alike fragment preserving attribution as label preservation, same-license propagation as derivative closure, and the BY-SA witness as a residual-stable certificate.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Altering the order of truth closure, admissibility, value refinement, quotienting, and certification produces different resulting semantics, as shown by the paper's finite examples.
  • The certified choice mechanism provides a uniform way to handle both modal value preservation and license propagation rules without downstream restrictions.

Load-bearing premise

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, and the discounted value transformer is defined only over those certified witnesses.

What would settle it

A pair of states that preserve all the listed structures under value-refined modal bisimulation but differ in their optimal discounted values, or an approximate quotient where the value error exceeds the pseudometric distance between states.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 4 minor

Summary. The paper develops a finite modal semantics closing truth under admissible continuation (via gfp of a one-step predecessor over choice cells), refining by discounted value over certified choices (local witnesses), and certifying via residual and public-release tests. Value-refined modal bisimulation is defined as the coarsest local equivalence preserving formulas, the admissibility kernel, certified choices, Bellman values, greedy sets, residual certificates, and public release certificates. A canonical pseudometric is the unique fixed point of the Hausdorff-lifted choice-matching transformer on certified choices; its kernel coincides with the bisimulation and the optimal discounted value is one-Lipschitz w.r.t. it. Any approximate quotient has distance-bounded value error. Branching choice-cell and locus presentations embed choice in the model while the transition presentation is a conservative retraction. The same machinery is applied to a public share-alike fragment (attribution as label preservation, derivative closure, admissibility, BY-SA witness as residual-stable certificate). Finite examples illustrate sensitivity to ordering of truth, admissibility, value, quotienting, public derivation, and certification.

Significance. If the fixed-point constructions and Lipschitz claim hold, the work supplies a coherent framework combining classical modal bisimulation with quantitative value refinement and explicit certification, which may be useful for verification tasks involving branching choices or license compliance. The standard gfp and Hausdorff-lifted constructions on finite models, the conservative retraction property, and the provision of finite examples are positive features that make the claims checkable in principle.

minor comments (4)
  1. The abstract states that the pseudometric is 'the unique fixed point' of the Hausdorff-lifted transformer; the full paper should include an explicit equation or theorem number establishing uniqueness (e.g., via Banach or Knaster-Tarski) and confirm that the one-Lipschitz property follows directly from the fixed-point equation.
  2. The transition presentation is described as 'a conservative retraction'; a dedicated subsection should state the retraction map and prove that it preserves the admissibility kernel and certified choices.
  3. Notation for the one-step predecessor operator and the choice-cell compatibility relation is used without displayed equations in the abstract; the paper should introduce these with numbered definitions before the bisimulation clause.
  4. The public share-alike fragment re-uses the same engine; a short table or example contrasting the license-specific certificates with the general residual certificates would improve readability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the detailed summary of the manuscript, the positive assessment of its significance, and the recommendation of minor revision. The referee's understanding of the fixed-point constructions, the value-refined bisimulation, the canonical pseudometric, the conservative retraction property, and the application to public share-alike certificates is accurate. As no specific major comments are listed in the report, we have no individual points requiring rebuttal or revision at this time.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper defines the admissibility kernel via the classical greatest fixed point of a one-step predecessor operator, certified choices as local witnesses, the value-refined bisimulation explicitly as the coarsest equivalence preserving a listed collection of properties (formulas, kernel, choices, Bellman values, etc.), and the canonical pseudometric as the unique fixed point of a Hausdorff-lifted transformer whose kernel coincides with that bisimulation. These are standard fixed-point constructions in modal logic and coalgebra; the preservation properties hold by the definition of coarsest equivalence, the Lipschitz claim follows from the pseudometric construction, and no step reduces a claimed prediction or theorem to a fitted parameter, self-citation, or definitional renaming of its own inputs. The argument is self-contained against external benchmarks of bisimulation and value-function theory.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Only the abstract is available; no information on free parameters, axioms or invented entities can be extracted from the provided text.

pith-pipeline@v0.9.1-grok · 5773 in / 1243 out tokens · 32875 ms · 2026-06-27T19:58:55.653792+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Layer Order Semantics for Automata-Based Cybersecurity

    cs.CR 2026-06 unverdicted novelty 6.0

    Introduces a layer-order automaton model that equates faithful online enforcement to regular prefix-closed languages under causal visibility and shows equivalence to deterministic edit automata while preserving layer-...

Reference graph

Works this paper leans on

54 extracted references · cited by 1 Pith paper

  1. [1]

    S. A. Kripke. Semantical analysis of modal logic I: normal modal propositional calculi. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 9:67–96, 1963

    1963

  2. [2]

    A. Tarski. A lattice-theoretical fixpoint theorem and its applications.Pacific Journal of Mathematics, 5(2):285–309, 1955

    1955

  3. [3]

    D. Kozen. Results on the propositional mu-calculus.Theoretical Computer Science, 27:333– 354, 1983

    1983

  4. [4]

    D. M. R. Park. Concurrency and automata on infinite sequences. InProceedings of the 5th GI Conference on Theoretical Computer Science, Lecture Notes in Computer Science 104, pages 167–183, Springer, 1981

    1981

  5. [5]

    Blackburn, M

    P. Blackburn, M. de Rijke, and Y. Venema.Modal Logic. Cambridge University Press, 2001

    2001

  6. [6]

    van Benthem.Modal Logic for Open Minds

    J. van Benthem.Modal Logic for Open Minds. CSLI Publications, 2010

    2010

  7. [7]

    A. Pnueli. The temporal logic of programs. InProceedings of the 18th Annual Symposium on Foundations of Computer Science, pages 46–57, 1977

    1977

  8. [8]

    E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. InLogic of Programs, Lecture Notes in Computer Science 131, pages 52–71, Springer, 1981

    1981

  9. [9]

    M. Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verifi- cation. InProceedings of the First Annual IEEE Symposium on Logic in Computer Science, pages 332–344, 1986

    1986

  10. [10]

    Baier and J.-P

    C. Baier and J.-P. Katoen.Principles of Model Checking. MIT Press, 2008

    2008

  11. [11]

    J. R. Buchi and L. H. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the American Mathematical Society, 138:295–311, 1969

    1969

  12. [12]

    Pnueli and R

    A. Pnueli and R. Rosner. On the synthesis of a reactive module. InProceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 179– 190, 1989. 70

    1989

  13. [13]

    E. A. Emerson and C. S. Jutla. Tree automata, mu-calculus and determinacy. InProceedings of the 32nd Annual Symposium on Foundations of Computer Science, pages 368–377, 1991

    1991

  14. [14]

    Bellman.Dynamic Programming

    R. Bellman.Dynamic Programming. Princeton University Press, 1957

    1957

  15. [15]

    Blackwell

    D. Blackwell. Discounted dynamic programming.The Annals of Mathematical Statistics, 36(1):226–235, 1965

    1965

  16. [16]

    M. L. Puterman.Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, 1994

    1994

  17. [17]

    D. P. Bertsekas.Dynamic Programming and Optimal Value Recursion. Athena Scientific, 4th edition, 2012

    2012

  18. [18]

    L. S. Shapley. Stochastic games.Proceedings of the National Academy of Sciences, 39(10):1095–1100, 1953

    1953

  19. [19]

    Aubin.Viability Theory

    J.-P. Aubin.Viability Theory. Birkhauser, 1991

    1991

  20. [20]

    Cousot and R

    P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. InConference Record of the Fourth ACM Symposium on Principles of Programming Languages, pages 238–252, 1977

    1977

  21. [21]

    Paige and R

    R. Paige and R. E. Tarjan. Three partition refinement algorithms.SIAM Journal on Com- puting, 16(6):973–989, 1987

    1987

  22. [22]

    Milner.Communication and Concurrency

    R. Milner.Communication and Concurrency. Prentice Hall, 1989

    1989

  23. [23]

    E. M. Clarke, O. Grumberg, and D. A. Peled.Model Checking. MIT Press, 1999

    1999

  24. [24]

    D. H. Wolpert and W. G. Macready. No free lunch theorems for optimization.IEEE Trans- actions on Evolutionary Computation, 1(1):67–82, 1997

    1997

  25. [25]

    L. C. Baird. Residual algorithms: reinforcement candidate selection with function approxi- mation. InProceedings of the Twelfth International Conference on Machine Learning, pages 30–37, Morgan Kaufmann, 1995

    1995

  26. [26]

    Pnueli and R

    A. Pnueli and R. Rosner. Distributed reactive systems are hard to synthesize. InProceedings of the 31st Annual Symposium on Foundations of Computer Science, pages 746–757, 1990

    1990

  27. [27]

    J. H. Reif. The complexity of two-player games of incomplete information.Journal of Com- puter and System Sciences, 29(2):274–301, 1984

    1984

  28. [28]

    Madani, S

    O. Madani, S. Hanks, and A. Condon. On the undecidability of probabilistic planning and related stochastic optimization problems.Artif. Intell., 147(1–2):5–34, 2003

    2003

  29. [29]

    Hennessy and R

    M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency.Journal of the ACM, 32(1):137–161, 1985

    1985

  30. [30]

    R. J. van Glabbeek. The linear time–branching time spectrum. InCONCUR 1990, Lecture Notes in Computer Science 458, pages 278–297, Springer, 1990

    1990

  31. [31]

    R. Alur, T. A. Henzinger, O. Kupferman, and M. Y. Vardi. Alternating refinement relations. InCONCUR 1998, Lecture Notes in Computer Science 1466, pages 163–178, Springer, 1998. 71

    1998

  32. [32]

    R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic.Journal of the ACM, 49(5):672–713, 2002

    2002

  33. [33]

    M. Pauly. A modal logic for coalitional power in games.Journal of Logic and Computation, 12(1):149–166, 2002

    2002

  34. [34]

    R. A. Howard.Dynamic Programming and Markov Processes. MIT Press, 1960

    1960

  35. [35]

    Grädel, W

    E. Grädel, W. Thomas, and T. Wilke, editors.Automata, Logics, and Infinite Games. Lec- ture Notes in Computer Science 2500, Springer, 2002

    2002

  36. [36]

    Bloem, K

    R. Bloem, K. Chatterjee, T. A. Henzinger, and B. Jobstmann. Better quality in synthesis through quantitative objectives. InProc. 21st International Conference on Computer Aided Verification (CAV), Lecture Notes in Computer Science 5643, pages 140–156. Springer, 2009

    2009

  37. [37]

    Chatterjee, T

    K. Chatterjee, T. A. Henzinger, and M. Jurdziński. Mean-payoff parity games. InProc. 20th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 178–187. IEEE, 2005

    2005

  38. [38]

    G. N. Iyengar. Universal dynamic programming.Mathematics of Operations Research, 30(2):257–280, 2005

    2005

  39. [39]

    Altman.Constrained Markov Decision Processes

    E. Altman.Constrained Markov Decision Processes. Chapman and Hall/CRC, 1999

    1999

  40. [40]

    Bernet, D

    J. Bernet, D. Janin, and I. Walukiewicz. Permissive strategies: from parity games to invari- ance games.RAIRO – Theoretical Informatics and Applications, 36(3):261–275, 2002

    2002

  41. [41]

    Fagin, J

    R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi.Reasoning About Knowledge. MIT Press, 1995

    1995

  42. [42]

    Chatterjee, L

    K. Chatterjee, L. Doyen, T. A. Henzinger, and J.-F. Raskin. Algorithms for omega-regular games with imperfect information.Logical Methods in Computer Science, 3(3:4):1–23, 2007

    2007

  43. [43]

    Niwiński and I

    D. Niwiński and I. Walukiewicz. Games for theµ-calculus.Theoretical Computer Science, 163(1–2):99–116, 1996

    1996

  44. [44]

    Chatterjee, T

    K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic.Information and Compu- tation, 208(6):677–693, 2010

    2010

  45. [45]

    van der Hoek and M

    W. van der Hoek and M. Wooldridge. Cooperation, knowledge, and time: Alternating-time temporal information logic and its applications.Studia Logica, 75:125–157, 2003

    2003

  46. [46]

    Kwiatkowska, G

    M. Kwiatkowska, G. Norman, and D. Parker. PRISM 4.0: Verification of probabilistic real- time systems. InComputer Aided Verification, Lecture Notes in Computer Science 6806, pages 585–591, Springer, 2011

    2011

  47. [47]

    Kwiatkowska, G

    M. Kwiatkowska, G. Norman, D. Parker, and G. Santos. PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time. InComputer Aided Verification, Lecture Notes in Computer Science 12225, pages 475–487, Springer, 2020

    2020

  48. [48]

    Artzner, F

    P. Artzner, F. Delbaen, J.-M. Eber, and D. Heath. Coherent measures of risk.Mathematical Finance, 9(3):203–228, 1999

    1999

  49. [49]

    Ruszczyński

    A. Ruszczyński. Risk-averse dynamic programming for Markov decision processes.Mathe- matical Programming, 125:235–261, 2010. 72

    2010

  50. [50]

    Desharnais, V

    J. Desharnais, V. Gupta, R. Jagadeesan, and P. Panangaden. Metrics for labelled Markov processes.Theoretical Computer Science, 318(3):323–354, 2004

    2004

  51. [51]

    van Breugel and J

    F. van Breugel and J. Worrell. A behavioural pseudometric for probabilistic transition systems.Theoretical Computer Science, 331(1):115–142, 2005

    2005

  52. [52]

    Ferns, P

    N. Ferns, P. Panangaden, and D. Precup. Metrics for finite Markov decision processes. In Proceedings of the 20th Conference on Uncertainty in Artificial Intelligence (UAI), pages 162–169, 2004

    2004

  53. [53]

    https://creativecommons.org/licenses/by-sa/4.0/

    Creative Commons.Attribution–ShareAlike 4.0 International (CC BY-SA 4.0): Deed. https://creativecommons.org/licenses/by-sa/4.0/

  54. [54]

    https://creativecommons.org/licenses/by-sa/4.0/legalcode.en

    Creative Commons.Attribution–ShareAlike 4.0 International (CC BY-SA 4.0): Legal Code. https://creativecommons.org/licenses/by-sa/4.0/legalcode.en. 73