Exact Safe Reachability for Discrete Storage Systems with a Fixed Total Input
This paper studies a discrete storage system with known contraction factor, nonnegative interval inputs, and a prescribed total input over a finite window. The complete input vector is fixed initially and remains unobserved. Safe suffix totals form a closed interval whose upper endpoint is concave and piecewise affine, with at most n+1 pieces and an explicit backward recursion. Forward propagation of the joint storage and remaining total gives exact polygons with O(T) edges. Intersecting forward and backward sets is equivalent to the existence of one complete safe path, which can be reconstructed by one-dimensional interval operations. A 2T-edge family attains the linear boundary order for explicit polygon representations. The construction also yields the pointwise earliest causal rule that never alarms on a safe window under path-independent observation schedules, including delayed and missing messages. OpenAI Codex assisted with mathematical derivation, proof organization, internal checking, and manuscript preparation.
Authors
- Zihuan Xu
Institutions
- Capital Normal University (CN)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-11-03
- DOI
- https://doi.org/10.5281/zenodo.23917875
- Primary Topic
- Formal Methods in Verification
- Type
- preprint