FPRD LabShare an approach

Regular stack certificates for bounded synchronization

Research note, 30 September 2026. A written extension of the one-counter certificate theorem, using classical regular pushdown reachability. Literature novelty is not established.

Contents

1. Retaining the contents of memory

Equal stack heights do not imply equal future behavior. A rule might pop only an A, or push only above a B. Forgetting the symbols may enable runs that the source could never execute. Our previous periodic height rows cannot express these distinctions.

Consider stacks written with their top at the left. A source can maintain the language (AB)* in its main state: push B and then A to add a pair, or pop A and then B to remove one. At either intermediate state its stack belongs to B(AB)*. Both symbols occur, at arbitrarily large depth. A rule that pushes on x only when the main state’s top is B can never execute. Erasing the top-symbol guard makes that rule look repeatable without bound.

Regular languages describe these possible stack contents with finite automata. This note proves that regular stack languages provide complete finite certificates for bounded height disagreement with a fixed input clock, for arbitrary finite stack alphabets. The certificate is verified offline. It does not replace an unbounded live stack by a finite state.

2. Exact model and certificate

Fix a normalized nondeterministic real-time pushdown source P. It has finite states Q, finite input alphabet Sigma, finite stack alphabet Gamma, nonempty initial state set I, and initially empty stack. A rule consumes one letter, tests the old state and either the old top symbol or emptiness, and performs one of: push a specified symbol, pop, or keep. A finite union of top tests is allowed as shorthand. Empty-stack pop is an explicitly permitted no-op; omit the empty guard to disable it. There are no epsilon moves, replacements, bulk actions or other tests. Acceptance is existential by state and, optionally, top symbol or emptiness.

Fix a complete finite input observer R, with initial state r0, update tau(r,a), and output c(r,a) in {-1,0,1}. It reads no stack or height and does not depend on the source’s choices. Its height starts at H=0 and updates to max(0,H+c). This reflected clock is the one used in the clock-inference note, not an absolute signed sum.

For a source configuration with stack w, set e=|w|-H. Represent the joint configuration by (q,r,e,w); its implicit clock height is |w|-e. A finite certificate assigns a regular language K(q,r,e) over Gamma to finitely many triples (q,r,e), where e is an integer. Omitted rows are empty. Each language is given by a finite automaton, which can be determinized and completed. The initial stack is the empty word epsilon; stack words are top-first.

There are three kinds of check.

Validity of coordinates. Every w in K(q,r,e) satisfies |w|>=e. For e<=0 this is automatic. For positive e it is a regular-language inclusion into the set of words of length at least e. Thus every listed stack represents a nonnegative clock height.

Initialization. For every q in I, epsilon belongs to K(q,r0,0).

Closure. For every row, input letter and outgoing source rule, split its domain according to the actual old top t in Gamma or empty, and according to whether the clock is zero or positive. Use only top cases allowed by the rule. For clock zero restrict to |w|=e; for clock positive restrict to |w|>e. Both conditions define regular sets, and the zero case is empty if e<0. Call the resulting intersection with K(q,r,e) the domain D.

On a fixed case the actual source height increment d and clock increment k are constants:

d={1push,−1pop with a nonempty top,0keep or empty pop,k={0c=−1 and clock zero,cotherwise.(1) d=\begin{cases}1&\text{push},\\ -1&\text{pop with a nonempty top},\\ 0&\text{keep or empty pop},\end{cases} \qquad k=\begin{cases}0&c=-1\text{ and clock zero},\\c&\text{otherwise}. \end{cases} \tag{1}

Let f be the stack update: f(w)=beta w for a push of beta; f(tu)=u for a nonempty pop; f(w)=w for a keep or empty pop. Put

e′=e+d−k,r′=τ(r,a). e'=e+d-k,\qquad r'=\tau(r,a).

For the rule’s new source state q’, check

f(D)⊆K(q′,r′,e′).(2) f(D)\subseteq K(q',r',e'). \tag{2}

There are finitely many cases. Intersections with top and length conditions are regular. Prefixing, removing a fixed first symbol, and identity preserve regularity effectively. Automata inclusion therefore decides (2), including when the target row is missing. A failing case supplies a specific old stack whose successor is excluded. This stack need not be reachable: rejection disproves the proposed invariant, not boundedness of the source.

For explicit DFA implementations, inclusion can also be checked without building image automata. Traverse a finite product recording the old row’s DFA state, the target DFA state after f of the prefix read so far, and the word length capped at max(e,0)+1. For a push, start the target DFA after reading beta; for a pop skip the first source symbol. The top case restricts the first symbol, and the final capped length determines the clock case. A reachable accepting-old/rejecting-target state gives a counterexample. Exhausting this finite product decides the unbounded inclusion.

3. The theorem

Theorem. For every P and fixed (R,c) just specified, the following are equivalent:

  1. There is B in N such that every finite legal run rho on every input u satisfies ||stack_rho(u)|-H(u)|<=B.
  2. A finite regular stack certificate passes all three checks above.

A passing certificate proves B=max |e| over its nonempty rows. Conversely, if a particular B is valid, a passing certificate exists using only displacements in [-B,B]. Certificate bounds need not be minimum.

All finite runs count, including rejecting runs, the empty run, and prefixes of runs that subsequently get stuck. The equivalence concerns a specified pushdown presentation and fixed input clock. It is not a characterization of languages admitting a bounded persistent implementation.

Soundness

Induct on any legal input run. Initialization gives its first row. Suppose its current stack belongs to the asserted row. Coordinate validity gives H=|w|-e>=0, so exactly one clock case applies. Its actual top picks an enabled source case. Formula (1) gives the true clamped increments, hence the true successor displacement e’. Inclusion (2) places the successor in its target row. Every prefix is therefore represented, and the finite set of row indices bounds the displacement.

Completeness: why the bounded product is pushdown

Suppose B is valid. Consider joint configurations with -B<=e<=B and H>=0, using (q,r,e) as finite control and the actual source stack w as the sole unbounded store. Retain exactly the source-clock steps that stay inside this corridor. A transition must test the source top and whether H=0, equivalently whether |w|=e. It may also need to reject a malformed |w|<e.

These tests are bounded-depth tests: e<=B, so inspecting at most B+1 source symbols distinguishes every length at most B from all greater lengths. For negative e the clock is necessarily positive. Top-symbol tests are included in the same inspection, also when B=0.

Here is an ordinary pushdown implementation of each such transition for offline reachability. Append a bottom marker. From a distinguished ready mode (q,r,e), select a source rule and enter its private inspection modes. Temporarily remove at most B+1 symbols, retaining their exact word in finite control; stop earlier on seeing the bottom marker, which is never removed. The finite observation determines the top, the necessary length tests, and the resulting displacement. Restore the removed symbols in reverse removal order. If the guard, coordinate validity or corridor test fails, do not return to a ready mode. Otherwise apply the selected source push, pop or keep and enter the ready mode (q’,tau(r,a),e’).

There are finitely many removed words of length at most B+1, hence finitely many private modes. Restoring or testing the bottom uses ordinary top rewrites, and no other source rule can interleave inside a private mode. Every successful ready-to-ready macro is exactly one original joint step. Every original step inside the corridor has such a macro. A failed inspection can at most reach a private dead end; it cannot create a spurious ready configuration. Starting from the finite initial ready set, induction gives an exact correspondence at ready modes. Input labels may be retained at macro entry for this correspondence and then erased for reachability.

This is a pushdown system with finite control, so the classical regular post* theorem applies to its finite initial set. Restrict its regular reachable configurations to each ready mode and remove the final bottom marker. This produces regular languages K(q,r,e) of exactly the reachable source stacks at that mode. No regularity is asserted for an unrestricted product of two pushdown stores.

These rows satisfy coordinate validity and initialization. Each enabled original successor of a reachable ready configuration is reachable in the original joint system. By the assumed bound it stays in the corridor, so the exact macro correspondence makes it reachable in the pushdown encoding. It therefore belongs to its row. All closure checks pass. QED.

The use of B in this existence proof is not circular certificate checking: the checker receives explicit finite automata and verifies every inclusion directly. It assumes neither reachability nor the desired bound.

What can be decided

Given P,R,c and B, construct the corridor pushdown system, compute its exact reachable ready languages by saturation, and check all original transition inclusions. A run leaving the corridor has a first-exit predecessor reachable inside it; that predecessor witnesses a failed inclusion. Thus this is a complete fixed-bound test, as was the previous VPA first-exit construction.

Without a supplied B, enumeration of finite regular certificates is a semidecision procedure. Fair enumeration of clocks can also search for a clock with a certificate. Neither yields a terminating negative answer or a computable upper bound on the required B. Positive semidecidability was already available by testing B=0,1,…; it is not an additional decidability result of this note.

4. Exact compilation guarantee

The certificate supplies a bound for the earlier source-normalization theorem. Annotate each input letter with the old observer state, keep at most 2B+1 source symbols in finite control above the synchronized core, apply visibly pushdown determinization, and produce the annotations online. This gives a deterministic real-time pushdown recognizer over the original alphabet. The offline inspection macros from the completeness proof are not used as the real-time recognizer.

Immutable cons records implement the resulting deterministic stack: one root, one pointer per record, at most one fresh record per input letter, and old access to the root and its tail. The reviewed simultaneous-record compiler gives a scaffold of degree two, native distance two, and one new physical node per letter. Finite control and labels may grow with the source, clock and B. These are construction bounds, not optima. Empty stack is a missing root with the compiler’s fixed virtual initialization; no extra input symbol is needed and the empty-prefix decision is preserved.

The scaffold accepts L(P) on the same words. The scaffold-to-PEG transfer gives a PEG for L(P)^R. Acceptance under the fixed compiled controller is preserved at every prefix; individual nondeterministic histories and raw stored-graph observations under arbitrary future scaffold contexts are not preserved by this determinization. The record compiler preserves its decoded deterministic stack. The certificate is an offline justification, not a runtime method for replaying or adapting all past computations.

5. Examples that test the symbol distinction

Here are the complete rules for the opening example. States are main, build and drain. Start in main with empty stack and accept there exactly when empty. Guards described as any include empty; all other guards are literal top symbols.

State Letter Guard Action New state
main a any push B build
build c B push A main
main b A pop drain
drain d B pop main
main x any keep main
main x B push B main

Use the one-state clock a,c=+1; b,d=-1; x=0. Set e=0 in all rows, with K(main)=(AB)* and K(build)=K(drain)=B(AB). Initialization and coordinate validity hold. Pushes prefix B then A; pops remove A then B; x keeps the stack, and the extra x-push has empty domain. These statements check (2) for every rule, proving B=0 at unbounded height. The language is nonregular: its intersection with (ac)(bd)* is {(ac)n(bd)n:n>=0}.

After erasing top symbols but retaining the nonempty restriction, the abstract source can read ac and then take the x-push arbitrarily often. The fixed clock remains at height two. Thus a correct analysis of that height abstraction cannot prove the true boundedness of the original source. The obstruction is caused by this abstraction, not by the language.

The main-state stacks AB and BA have equal height, but only AB belongs to the invariant. BA would enable the extra x-push. Even preserving just the allowed top of each state is insufficient for these proposed coarse rows: K(main)={epsilon} union A Gamma, K(build)=K(drain)=B Gamma. They include the stack A in main, whose b-pop produces empty stack in drain and violates closure. Regular rows retain the symbol relations needed after future pops. This is a failure of those coarse rows, not an impossibility theorem for all finite summaries, encodings, or other certificates.

Other checks include the previous bottom pop/keep source, the guarded push-once source with B=1, and a clock that advances once while the source stays empty, giving e=-1. Unary regular rows recover the previous periodic certificate theorem after translating |w| to z=|w|-max(e,0).

Independent push/keep remains a genuine negative presentation: after x^n there are legal heights 0 and n, so any input clock is at distance at least n/2 from one. No finite regular certificate exists. If all states accept, its language is x*, so this says nothing against other presentations of that language. A rejected finite candidate alone would not prove this unboundedness; the family of runs does.

6. Contribution, verification and next bottleneck

The imported theorem is regular forward reachability of pushdown systems. Schwoon’s Model-Checking Pushdown Systems (2002), Theorems 3.3 and 3.5, gives correctness and effective construction of post*. These statements were inspected in the primary thesis. The earlier work of Bouajjani, Esparza and Maler and of Esparza, Hansel, Rossmanith and Schwoon underlies this method. Regular-language closure and private finite-control expansions are standard automata constructions. VPA determinization is imported through the earlier normalization argument from Alur and Madhusudan.

The additional argument is the exact reflected-clock encoding, its complete regular certificate interface, and its composition with the explicit scaffold resource guarantee. This extension is a direct application of established reachability methods, not evidence of a new reachability theorem or a new automata class. Literature priority has not been established. The prior residual/bisimulation, persistence, pointer-machine and uniformization comparisons retain their scope in the foundational contracts. This theorem makes no representation-independent lower bound or generalized pumping assertion.

The checker implements exact DFA inclusion checks on supplied certificates and returns counterexample stacks. Its recorded output includes the actual certificate automata, positive examples, invalid candidates, and the exact scope of bounded implementation audits. Exhausting a finite product is an exact inclusion decision; the finite audits only corroborate that implementation. The written theorem is not proof-assistant verified. The executable does not implement saturation, certificate synthesis, VPA determinization or scaffold generation.

This closes the stack-content extension. The decisive remaining question is whether bounded skew relative to a fixed reflected input clock is decidable when B is not supplied, even for one-counter sources. A useful next result would give a computable bound on B for every bounded instance, or an appropriately scoped obstruction to such a decision. Increasing certificate vocabulary again would not resolve that bottleneck.

Primary dependencies: