pith. sign in

arxiv: 2606.25979 · v1 · pith:IKEWVCA7new · submitted 2026-06-24 · 💻 cs.FL

Monitoring Discounted Sum Properties

Filip Cano , Thomas A. Henzinger , Konstantin Kueffner , N. Ege Sara\c{c} This is my paper

Pith reviewed 2026-06-25 19:56 UTC · model grok-4.3

classification 💻 cs.FL
keywords runtime monitoringdiscounted sumsfinite memoryapproximate soundnessstochastic monitoringaffine register machinesalgorithmic fairness
0
0 comments X

The pith

Exact sound monitoring of discounted sums is impossible with finite memory, so the paper introduces ε-approximately sound monitoring with explicit resource bounds.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that runtime monitoring of discounted sums on sequential signals cannot achieve exact soundness with any finite amount of memory, because the running value depends on an unbounded history of past observations scaled by the discount factor. A sympathetic reader would care because discounted sums are meant to provide a stable yet local quantitative measure for properties like algorithmic fairness, avoiding both the noise of instantaneous values and the loss of structure in long-run averages. To make monitoring feasible, the authors define ε-approximately sound monitors and derive concrete bounds on the memory states and observation window needed to guarantee the approximation. They further extend the setting to stochastic processes by introducing pointwise and uniform (ε,δ)-soundness, prove statistical optimality results, and show an impossibility threshold beyond which no monitor works. Finally, they model the deterministic case with affine register machines to obtain a tight lower bound on resource use and supply a specification language for arithmetic expressions over several discounted sums.

Core claim

Exact, sound monitoring of discounted sums cannot be achieved with finite memory. To overcome this impossibility, we introduce ε-approximately sound monitoring, deriving explicit bounds on memory and observation requirements. We extend the framework to stochastic processes via expected discounted sums, defining pointwise and uniform (ε,δ)-soundness notions, establishing statistical optimality, and proving impossibility beyond a precision threshold. We formalize the resource complexity of deterministic discounted monitoring via affine register machines and prove a tight worst-case lower bound. We also present a specification language for arithmetic expressions over multiple discounted sums.

What carries the argument

ε-approximately sound monitoring, which relaxes exact tracking of the discounted sum by a tolerance ε while still guaranteeing soundness up to that tolerance, together with the impossibility proof that no finite-memory exact monitor exists.

If this is right

  • Any exact monitor for discounted sums must use unbounded memory.
  • For any desired ε>0 there exist finite-memory monitors whose size and observation window are bounded explicitly in terms of ε and the discount factor.
  • In the stochastic case, (ε,δ)-sound monitors achieve statistical optimality up to a precision threshold beyond which no monitor can succeed.
  • The worst-case resource cost of deterministic discounted monitoring is tightly characterized by the lower bound on affine register machines.
  • Arithmetic expressions combining several discounted sums admit both synchronous and asynchronous monitoring semantics.

Where Pith is reading between the lines

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

  • The same finite-memory barrier and ε-approximation technique may apply to other quantitative measures that accumulate history with decaying weights.
  • In fairness auditing, the explicit memory bounds let practitioners trade off monitor size against the tolerated error in fairness metrics.
  • The affine-register-machine characterization could be used to compare the cost of discounted-sum monitoring against other quantitative runtime-verification tasks.

Load-bearing premise

The monitoring problem assumes signals arrive sequentially online and the discount factor is fixed and known in advance.

What would settle it

Exhibiting a finite-state machine that, for some fixed discount factor, maintains a state from which the exact discounted sum can be recovered for every possible infinite input sequence would falsify the impossibility result.

read the original abstract

Runtime monitoring of quantitative signals faces a fundamental trade-off between volatility and over-aggregation: instantaneous observations are noisy, while long-run averages obscure local structure. Localisation measures such as discounted averages offer a principled middle ground, yet remain poorly understood in runtime verification. This paper studies discounted sums from a monitoring perspective, in both deterministic and stochastic settings. We formalize the discounted monitoring problem and show that exact, sound monitoring of discounted sums cannot be achieved with finite memory. To overcome this impossibility, we introduce $\varepsilon$-approximately sound monitoring, deriving explicit bounds on memory and observation requirements. We then extend the framework to stochastic processes via expected discounted sums, defining pointwise and uniform $(\varepsilon,\delta)$-soundness notions, establishing statistical optimality, and proving impossibility beyond a precision threshold. We also formalize the resource complexity of deterministic discounted monitoring via affine register machines and prove a tight worst-case lower bound. Finally, we present a specification language for arithmetic expressions over multiple discounted sums with synchronous and asynchronous semantics, and evaluate our approach on practical scenarios including algorithmic fairness.

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

3 major / 3 minor

Summary. The paper formalizes the discounted monitoring problem for quantitative signals in deterministic and stochastic settings. It proves that exact sound monitoring of discounted sums cannot be achieved with finite memory, introduces ε-approximately sound monitoring with explicit bounds on memory and observation requirements, extends the framework to expected discounted sums with pointwise and uniform (ε,δ)-soundness notions while establishing statistical optimality and an impossibility result beyond a precision threshold, analyzes resource complexity via affine register machines with a tight worst-case lower bound, and presents a specification language for arithmetic expressions over multiple discounted sums (with synchronous and asynchronous semantics) evaluated on practical scenarios including algorithmic fairness.

Significance. If the formal results hold, the work provides foundational contributions to runtime verification of quantitative properties by clarifying fundamental limitations of finite-memory monitoring for discounted sums and offering principled approximations with explicit resource bounds. The tight lower bound via affine register machines, the statistical optimality claims, and the specification language with evaluation are notable strengths that could influence monitoring tool design for properties balancing volatility and aggregation.

major comments (3)
  1. [deterministic impossibility section] The section on the deterministic impossibility result: the central claim that exact sound monitoring cannot be achieved with finite memory (under fixed known discount factor) is load-bearing for motivating the ε-approximate approach; the derivation must explicitly construct or argue why any finite-memory monitor fails on some signal sequence, including the role of the discount factor in the argument.
  2. [stochastic extension] The stochastic processes section: the definitions of pointwise and uniform (ε,δ)-soundness, the proof of statistical optimality, and the impossibility beyond a precision threshold require the full error analysis and evaluation details to substantiate the claims, as the abstract asserts these without visible supporting derivations or bounds.
  3. [complexity analysis] The affine register machine complexity section: the tight worst-case lower bound must be shown to match the upper bound construction exactly (e.g., via a specific family of expressions or discount factors), as this is presented as a key technical result.
minor comments (3)
  1. [specification language] Clarify the synchronous vs. asynchronous semantics in the specification language section with a small example.
  2. [evaluation] The evaluation on algorithmic fairness would benefit from explicit comparison metrics or baseline monitors to strengthen the practical claims.
  3. Ensure all notation for discounted sums, ε-approximations, and register machines is defined before first use and consistent across sections.

Simulated Author's Rebuttal

3 responses · 0 unresolved

We thank the referee for the detailed and constructive comments. We address each major comment below.

read point-by-point responses

  1. Referee: [deterministic impossibility section] The section on the deterministic impossibility result: the central claim that exact sound monitoring cannot be achieved with finite memory (under fixed known discount factor) is load-bearing for motivating the ε-approximate approach; the derivation must explicitly construct or argue why any finite-memory monitor fails on some signal sequence, including the role of the discount factor in the argument.

    Authors: The impossibility proof assumes an arbitrary finite-memory monitor and constructs an adversarial signal sequence on which soundness fails for some prefix. The discount factor γ ∈ (0,1) is central because it permits pairs of sequences whose discounted sums differ by an arbitrarily small amount while demanding distinct outputs. We will revise the section to present this construction explicitly, with a concrete family of sequences and a step-by-step argument showing why finite memory is insufficient. revision: yes

  2. Referee: [stochastic extension] The stochastic processes section: the definitions of pointwise and uniform (ε,δ)-soundness, the proof of statistical optimality, and the impossibility beyond a precision threshold require the full error analysis and evaluation details to substantiate the claims, as the abstract asserts these without visible supporting derivations or bounds.

    Authors: The definitions of pointwise and uniform (ε,δ)-soundness, the concentration inequalities establishing statistical optimality, and the impossibility threshold are derived in the main text and appendix. To make the supporting derivations fully visible without relying on the appendix, we will expand the main-body presentation of the error analysis and explicit bounds. revision: partial

  3. Referee: [complexity analysis] The affine register machine complexity section: the tight worst-case lower bound must be shown to match the upper bound construction exactly (e.g., via a specific family of expressions or discount factors), as this is presented as a key technical result.

    Authors: The lower-bound proof identifies a concrete family of arithmetic expressions over discounted sums (with discount factors in a fixed open interval) that force exactly as many affine registers as the upper-bound construction. We will revise the section to state this family explicitly and verify the matching resource count for each expression. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's core results—an impossibility theorem for finite-memory exact monitoring of discounted sums, followed by explicit bounds for ε-approximate soundness, extensions to stochastic (ε,δ)-soundness, affine register machine complexity, and a specification language—are derived from a standard formalization of online sequential observation with fixed known discount factor. No step reduces by construction to a fitted parameter, self-definition, or self-citation chain. The impossibility result and bounds follow from the stated model assumptions without renaming known results or smuggling ansatzes. The derivation is self-contained against external benchmarks (formal proofs and complexity arguments), yielding a normal non-finding.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claims rest on standard definitions from runtime verification and automata theory together with basic properties of discounted sums and expectation; no free parameters, ad-hoc axioms, or invented entities are indicated in the abstract.

axioms (1)
  • standard math Standard semantics of runtime monitoring and properties of discounted sums over sequences
    The formalization of the discounted monitoring problem and impossibility result presuppose established definitions in formal methods.

pith-pipeline@v0.9.1-grok · 5716 in / 1293 out tokens · 29191 ms · 2026-06-25T19:56:38.761739+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

46 extracted references · 3 canonical work pages

  1. [1]

    2009 , publisher=

    Real analysis: measure theory, integration, and Hilbert spaces , author=. 2009 , publisher=

    2009

  2. [2]

    2018 , publisher=

    High-dimensional probability: An introduction with applications in data science , author=. 2018 , publisher=

    2018

  3. [3]

    The Annals of Statistics , volume=

    Time-uniform, nonparametric, nonasymptotic confidence sequences , author=. The Annals of Statistics , volume=. 2021 , publisher=

    2021

  4. [4]

    Tohoku Mathematical Journal, Second Series , volume=

    Weighted sums of certain dependent random variables , author=. Tohoku Mathematical Journal, Second Series , volume=. 1967 , publisher=

    1967

  5. [5]

    2024 , url=

    Han, Xiaotian and Chi, Jianfeng and Chen, Yu and Wang, Qifan and Zhao, Han and Zou, Na and Hu, Xia , booktitle=. 2024 , url=

    2024

  6. [6]

    2020 , booktitle =

    Data Center Power Oversubscription with a Medium Voltage Power Plane and Priority-Aware Capping , author =. 2020 , booktitle =

    2020

  7. [7]

    Proceedings Eighth International Symposium on High Performance Computer Architecture , pages=

    Control-theoretic techniques and thermal-RC modeling for accurate and localized dynamic thermal management , author=. Proceedings Eighth International Symposium on High Performance Computer Architecture , pages=. 2002 , organization=

    2002

  8. [8]

    Alamdari and Toryn Q

    Parand A. Alamdari and Toryn Q. Klassen and Elliot Creager and Sheila A. McIlraith , title =

  9. [9]

    ACM Transactions on Computational Logic (TOCL) , volume=

    Quantitative languages , author=. ACM Transactions on Computational Logic (TOCL) , volume=. 2010 , publisher=

    2010

  10. [10]

    International Colloquium on Automata, Languages, and Programming , pages=

    Discounting the future in systems theory , author=. International Colloquium on Automata, Languages, and Programming , pages=. 2003 , organization=

    2003

  11. [11]

    Leibniz International Proceedings in Informatics , volume=

    Approximate determinization of quantitative automata , author=. Leibniz International Proceedings in Informatics , volume=

  12. [12]

    Proceedings of the national academy of sciences , volume=

    Stochastic games , author=. Proceedings of the national academy of sciences , volume=. 1953 , publisher=

    1953

  13. [13]

    2012 , publisher=

    Competitive Markov decision processes , author=. 2012 , publisher=

    2012

  14. [14]

    International conference on tools and algorithms for the construction and analysis of systems , pages=

    Discounting in LTL , author=. International conference on tools and algorithms for the construction and analysis of systems , pages=. 2014 , organization=

    2014

  15. [15]

    2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science , pages=

    The target discounted-sum problem , author=. 2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science , pages=. 2015 , organization=

    2015

  16. [16]

    International Journal of Foundations of Computer Science , volume=

    Reachability problems for one-dimensional piecewise affine maps , author=. International Journal of Foundations of Computer Science , volume=. 2018 , publisher=

    2018

  17. [17]

    Logical Methods in Computer Science , volume=

    Comparator automata in quantitative verification , author=. Logical Methods in Computer Science , volume=. 2022 , publisher=

    2022

  18. [18]

    Lectures on Runtime Verification: Introductory and Advanced Topics , pages=

    Introduction to runtime verification , author=. Lectures on Runtime Verification: Introductory and Advanced Topics , pages=. 2018 , publisher=

    2018

  19. [19]

    International symposium on formal techniques in real-time and fault-tolerant systems , pages=

    Monitoring temporal properties of continuous signals , author=. International symposium on formal techniques in real-time and fault-tolerant systems , pages=. 2004 , organization=

    2004

  20. [20]

    Theoretical Computer Science , volume=

    Robustness of temporal logic specifications for continuous-time signals , author=. Theoretical Computer Science , volume=. 2009 , publisher=

    2009

  21. [21]

    International conference on formal modeling and analysis of timed systems , pages=

    Robust satisfaction of temporal logic over real-valued signals , author=. International conference on formal modeling and analysis of timed systems , pages=. 2010 , organization=

    2010

  22. [22]

    International conference on computer aided verification , pages=

    Efficient robust monitoring for STL , author=. International conference on computer aided verification , pages=. 2013 , organization=

    2013

  23. [23]

    Formal Methods in System Design , volume=

    Robust online monitoring of signal temporal logic , author=. Formal Methods in System Design , volume=. 2017 , publisher=

    2017

  24. [24]

    2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages=

    Quantitative and approximate monitoring , author=. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , pages=. 2021 , organization=

    2021

  25. [25]

    Technometrics , volume=

    Control chart tests based on geometric moving averages , author=. Technometrics , volume=. 2000 , publisher=

    2000

  26. [26]

    1989 , publisher=

    Discrete-time signal processing , author=. 1989 , publisher=

    1989

  27. [27]

    Technometrics , volume=

    Exponentially weighted moving average control schemes: properties and enhancements , author=. Technometrics , volume=. 1990 , publisher=

    1990

  28. [28]

    2020 , publisher=

    Introduction to statistical quality control , author=. 2020 , publisher=

    2020

  29. [29]

    International journal of forecasting , volume=

    Exponential smoothing: The state of the art—Part II , author=. International journal of forecasting , volume=. 2006 , publisher=

    2006

  30. [30]

    Journal of statistical software , volume=

    Automatic time series forecasting: the forecast package for R , author=. Journal of statistical software , volume=

  31. [31]

    arXiv preprint arXiv:2504.01154 , year=

    Remember, but also, Forget: Bridging Myopic and Perfect Recall Fairness with Past-Discounting , author=. arXiv preprint arXiv:2504.01154 , year=

    arXiv

  32. [32]

    Usman Gohar and Zeyu Tang and Jialu Wang and Kun Zhang and Peter Spirtes and Yang Liu and Lu Cheng , title =. Trans. Mach. Learn. Res. , year =

  33. [33]

    Proceedings of the AAAI Conference on Artificial Intelligence , volume=

    Achieving long-term fairness in sequential decision making , author=. Proceedings of the AAAI Conference on Artificial Intelligence , volume=

  34. [34]

    International conference on machine learning , pages=

    Fairness in reinforcement learning , author=. International conference on machine learning , pages=. 2017 , organization=

    2017

  35. [35]

    Ethics in Artificial Intelligence: Bias, Fairness and Beyond , pages=

    Temporal Fairness in Online Decision-Making , author=. Ethics in Artificial Intelligence: Bias, Fairness and Beyond , pages=. 2023 , publisher=

    2023

  36. [36]

    International Conference on Machine Learning , pages=

    Delayed impact of fair machine learning , author=. International Conference on Machine Learning , pages=. 2018 , organization=

    2018

  37. [37]

    Torres and Parisa Zehtabi and Michael Cashmore and Daniele Magazzeni and Manuela Veloso , title =

    Manuel R. Torres and Parisa Zehtabi and Michael Cashmore and Daniele Magazzeni and Manuela Veloso , title =. European Conference of Artificial Intelligence (

  38. [38]

    International Conference on Computer Aided Verification , pages=

    Monitoring algorithmic fairness , author=. International Conference on Computer Aided Verification , pages=. 2023 , organization=

    2023

  39. [39]

    International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=

    Stream-Based Monitoring of Algorithmic Fairness , author=. International Conference on Tools and Algorithms for the Construction and Analysis of Systems , pages=. 2025 , organization=

    2025

  40. [40]

    Advances in neural information processing systems , volume=

    Equality of opportunity in supervised learning , author=. Advances in neural information processing systems , volume=

  41. [41]

    Proceedings of the 3rd innovations in theoretical computer science conference , pages=

    Fairness through awareness , author=. Proceedings of the 3rd innovations in theoretical computer science conference , pages=

  42. [42]

    1996 , howpublished =

    Becker, Barry and Kohavi, Ronny , title =. 1996 , howpublished =

    1996

  43. [43]

    Formal Methods in System Design , volume=

    A survey of challenges for runtime verification from advanced application domains (beyond software) , author=. Formal Methods in System Design , volume=. 2019 , publisher=

    2019

  44. [44]

    Michael Kaminski and Nissim Francez , title =. Theor. Comput. Sci. , volume =. 1994 , url =. doi:10.1016/0304-3975(94)90242-9 , timestamp =

    work page doi:10.1016/0304-3975(94)90242-9 1994

  45. [45]

    Deshmukh and Mukund Raghothaman and Yifei Yuan , title =

    Rajeev Alur and Loris D'Antoni and Jyotirmoy V. Deshmukh and Mukund Raghothaman and Yifei Yuan , title =. 28th Annual. 2013 , url =. doi:10.1109/LICS.2013.65 , timestamp =

    work page doi:10.1109/lics.2013.65 2013

  46. [46]

    A Theory of Register Monitors , booktitle =

    Thomas Ferr. A Theory of Register Monitors , booktitle =. 2018 , url =. doi:10.1145/3209108.3209194 , timestamp =

    work page doi:10.1145/3209108.3209194 2018