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

Institutions

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
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
preprint

Exact Safe Reachability for Discrete Storage Systems with a Fixed Total Input

Zihuan Xu
Zenodo (CERN European Organization for Nuclear Research)
Formal Methods in Verification
preprint

Exact Safe Reachability for Discrete Storage Systems with a Fixed Total Input

Zihuan Xu
preprint en

Abstract

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.

Zenodo (CERN European Organization for Nuclear Research)
Capital Normal University (CN)
Formal Methods in Verification
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

Laika access coming soon