Inferring stack clocks from finite control

Research note, 29 September 2026. This continues the bounded-skew construction. The arguments below are mathematical proofs, not proof-assistant certificates. No literature-priority claim is made.

1. From a supplied clock to a checkable certificate

Consider a machine that pushes on the first block of a letters, switches phase on #, and pops on the second block. Its stack timing is determined by the input, but a single call/return classification of a cannot describe it. A two-state input observer can: before #, output a call for a; afterwards, output a return. This familiar example suggests letting a finite input observer provide the clock.

There is a harder issue when the source has several possible stack timings. The previous note proves that a supplied clock works if every source run stays within a supplied bound B of it. Here we give a finite sufficient test that can infer both the clock and B. The test uses the source’s finite control graph, so it can succeed without exploring its unbounded stacks. Ignoring stack guards makes it conservative.

The result is an effective certificate class for specified presentations. It is not an intrinsic characterization of languages or of all bounded-skew presentations. A failed search within this class is inconclusive outside it.

2. Exact source and clock models

The source P has finite control Q, a finite stack alphabet, a nonempty finite initial-state set I, and an initially empty stack. It is nondeterministic, real-time, and has no epsilon transitions. Each rule consumes one letter, tests the state and top symbol or emptiness, and pushes one symbol, pops one symbol, or leaves the stack unchanged. A pop at bottom is either disabled or an explicitly permitted no-op. There are no replacements of the top symbol, bulk actions, identity queries, or hidden computation between letters. Acceptance is existential, by state and optionally top symbol or emptiness.

Each rule e has a nominal action d(e) in {-1,0,1}: pop, keep, or push. In particular a permitted bottom-pop still has nominal action -1. Along every legal run, the actual height satisfies

$$h_0=0,\qquad h_{j+1}=\max(0,h_j+d(e_{j+1})). \tag{1}$$

A clock consists of a complete deterministic input observer R=(S,s_0,tau), with tau:S x Sigma -> S, and an output table c:S x Sigma -> {-1,0,1}. It reads only the input. Writing s_j=tau(s_{j-1},a_j), its height is

$$H_0=0,\qquad H_j=\max(0,H_{j-1}+c(s_{j-1},a_j)). \tag{2}$$

The observer does not read the source state, stack, or nondeterministic choice. Its finite state does not depend on clock height. This is a reflected unit-action clock; it is not the absolute value of a signed sum. For example repeated returns give height zero here, while the absolute value of their signed sum grows without bound.

Build the reachable finite product graph G on Q x S, starting at I x {s_0}. For each source rule e:q –a,d–> q’, insert

$$(q,s)\longrightarrow(q',\tau(s,a)),\qquad w(e,s)=d(e)-c(s,a). \tag{3}$$

Retain parallel rules. Discard stack guards when forming G, but do not invent source rules. Thus every legal source run is a path of G, although a path of G need not be a legal run. Let N be the number of its reachable vertices.

3. Finite-cycle certificate and the resulting theorem

The certificate condition is:

$$\text{every reachable directed cycle of G has total weight zero.} \tag{Z}$$

Let l and u be the minimum and maximum weights of all finite paths from I x {s_0}, including zero-length paths. Under (Z), these extrema exist and are computable. Put B=u-l.

Theorem. For every source P and finite observer/output table (R,c) satisfying (Z), every legal finite source run rho on every word w satisfies

$$|h_\rho(w)-H(w)|\leq B=u-l\leq4(N-1). \tag{4}$$

The hypotheses are decidable directly on the finite product graph. For a fixed observer transition table, existence of an output table satisfying (Z) is decidable. For every supplied positive observer-state budget m, existence of such a certificate using at most m observer states is decidable. These searches require no supplied skew bound.

Every successful certificate effectively gives a deterministic real-time pushdown recognizer for L(P), and hence a degree-two, distance-two scaffold with one new physical node per input letter. It gives a PEG for L(P)^R. The bounds are construction bounds, not optima. The preservation assertion is same-word acceptance at every prefix, including the empty prefix, followed by one reversal in the PEG transfer. It is not equivalence of raw stored graphs under arbitrary testing contexts.

Proof of the path bound

In a finite directed graph, all path weights from the initial set are bounded above and below if and only if every reachable directed cycle has weight zero. For necessity, repeat a reachable nonzero cycle arbitrarily often. For sufficiency, remove closed subwalks from any path. Every closed subwalk decomposes into directed simple cycles and hence has weight zero. The result is a simple path with the same weight and at most N-1 edges.

Each edge has weight between -2 and 2. Therefore

$$-2(N-1)\leq l\leq0\leq u\leq2(N-1). \tag{5}$$

The iff here concerns weights on the abstract graph. It does not concern actual stack heights or language recognition.

Proof at the bottom boundary

For one legal run of length n, let X_j be the cumulative nominal source actions and Y_j the cumulative clock outputs, with X_0=Y_0=0. Every prefix is a path of G, so l <= X_j-Y_j <= u. Recurrences (1)-(2) have the elementary reflection formulas

$$h_n=X_n-\min_{0\leq j\leq n}X_j,\qquad H_n=Y_n-\min_{0\leq j\leq n}Y_j. \tag{6}$$

The minima already include zero. Induction verifies (6), including a pop at bottom. The pointwise inequalities imply

$$l\leq\min_jX_j-\min_jY_j\leq u.$$

Subtracting this quantity from X_n-Y_n gives (4). This is the discrete one-sided reflection argument, a standard ingredient rather than a new reflection theorem. Crucially, bounded signed discrepancy must be proved at all prefixes. A final-net comparison alone does not suffice.

Deciding and synthesizing certificates

For a candidate (R,c), compute shortest and longest path values from the initial set by N-1 rounds of edge relaxation, retaining shorter paths each round. If either value improves on the Nth round, a reachable negative or positive cycle exists. Otherwise the attained minima and maxima give l,u. Equivalently, within each strongly connected component the edge weights admit an additive vertex potential; paths between components account for the remaining finite offsets.

Do not demand one global exact potential on an arbitrary graph. Two acyclic paths can reach the same vertex with different weights while all path weights remain bounded. The min/max procedure handles these joins.

For a fixed observer R there are 3^(|S||Sigma|) possible output tables. Enumerate them and test (Z). For a state budget m, enumerate k=1,…,m, all complete transition tables on k named states with initial state 0, and all output tables. There are (3k)^(k|Sigma|) candidates for each k. This is a finite decision procedure for existence within this certificate class. It does not decide existence of any finite-state clock with bounded actual height skew. It also does not decide existence with unbounded observer size.

All returned certificates carry finite min/max path bounds that can be checked against every edge. No deterministic realization is assumed during the test.

4. Why a finite-state clock still compiles in one step

This part does not require (Z). Suppose any supplied (R,c,B) satisfies the every-prefix, every-legal-run corridor condition (4).

Annotate a word online by

$$E_R(a_1\cdots a_n)=(s_0,a_1)(s_1,a_2)\cdots(s_{n-1},a_n).$$

On the finite alphabet S x Sigma, give (s,a) the visible action c(s,a). Form an annotated source that runs P and rejects an annotation inconsistent with tau and s_0. It is real-time and has the same stack alphabet; every legal run is now within B of an ordinary visible clock. The previous bounded-skew proof applies verbatim: keep at most 2B+1 source symbols in finite control above a core cut at max(0,H-B-1), using dummy frames and saved capped-height tags. It gives a VPA over the annotated alphabet.

Determinize that VPA by the classical theorem, then compute E_R online in finite control while simulating it. This consumes exactly one original letter for each annotated letter. Each step performs at most one unit stack action; no lookahead, epsilon work, or initialization letter is introduced. The resulting machine over Sigma is a deterministic real-time PDA. It need not be visibly pushdown on the original alphabet, because action can depend on the observer state.

Immutable linked records implement its stack with one root, one pointer per record and at most one allocation per letter. Source access reaches at most the old root and its tail. The reviewed record compiler with s=A=q=r=1 gives degree two and distance two. Its finite control includes the observer, buffer/determinization data and acceptance flags. Empty logical stack is a missing root, requiring no nonempty initial graph. The compiler preserves the decoded deterministic stack and acceptance. Determinization preserves existential acceptance, not an individual nondeterministic history.

For a fixed finite-state clock and fixed B, the previous first-exit VPA also works on annotated inputs, giving a complete corridor test for that fixed pair. This is distinct from the conservative finite-cycle inference test. Several sources with the same clock can similarly be normalized on the same annotated alphabet before using Boolean closure or selector coverage.

5. Positive examples and failures that delimit the test

Hidden early and late actions

The previous note’s source operates on prefixes of (ac)(bd). It chooses whether to push early or late in each ac pair and pop early or late in each bd pair. The visible choice a=+1, c=0, b=-1, d=0 makes every control cycle have zero discrepancy. Abstract prefix discrepancies range from -1 to 1, so the graph test produces B=2. The direct source argument proves the tighter B=1. This difference illustrates why the certificate bound is not claimed optimal. The accepted language is {(ac)^n(bd)n:n>=0}.

The same letter in two phases

Let P push on a in a build state, change to a drain state on #, and pop on a in that state, with pops disabled at bottom. Accept in the drain state exactly at empty stack. Thus L(P)={a^n#an:n>=0}.

Every one-state clock fails (Z): the build loop requires c(a)=+1, while the drain loop requires c(a)=-1. A two-state observer switching at # gives these two actions and c(#)=0. All reachable product-edge weights are zero, so the inferred B is zero. The clock is inferred from the phase structure, not from a supplied stack bound. This is the standard phase-dependent height-deterministic example, not a new language separation.

Genuine unbounded disagreement

In one state, allow either a push or a keep on each x, at every stack height. After x^n, legal runs reach both 0 and n. Every clock, including any finite-state clock, is farther than B from one of them for n>2B. The certificate fails, as it should. If all states accept, the language is x*, so this is a presentation obstruction only.

Bottom saturation defeats necessity

In one state, instead allow either a pop or a keep on each x, with a pop at bottom acting as a no-op. From empty initialization every legal run stays at height zero. The constant-zero clock works with B=0.

Nevertheless no finite observer can satisfy (Z). On repeated x, its state eventually cycles with some period p. Over that observer cycle, the all-keep abstract path has nominal sum 0 and the all-pop path has sum -p. They have the same clock sum, so both discrepancy sums cannot be zero. This excludes the certificate for every finite observer size, despite perfect actual height synchronization. It proves that the certificate class is strictly conservative even before stack guards are considered.

Stack guards also defeat necessity

A one-state source pushes on x only when empty and keeps on x only when nonempty. Its actual heights are 0 initially and 1 thereafter. The zero clock has B=1. Its guard-erased graph has independent push/keep x loops and fails the cycle certificate for the same reason as the unbounded example. Legal-run restrictions cannot be discarded for negative claims.

6. Literature comparison and contribution status

Nowotka and Srba, Height-Deterministic Pushdown Automata (2007), Section 4.1, describe Caucal’s earlier clock as an input-deterministic integer-output transducer with exact source height |T(w)|. Their Theorem 4 determinizes real-time height-deterministic PDA, and Example 1 gives the phase-dependent language used above. These are established precedents for input-dependent synchronization, not new contributions here.

The original Caucal 2006 full construction could not be retrieved in this run; its author-posted abstract confirms fixed-transducer synchronization testing and effective Boolean closure. That does not verify an equivalence with our reflected convention or settle priority for the bounded buffer. In particular |sum c| and (6) cannot be identified on arbitrary words. The annotation proof above avoids needing that identification. A detailed comparison with Caucal’s full construction remains open.

The zero-cycle path lemma is elementary weighted-graph theory. Equation (6) is the discrete one-sided Skorokhod reflection formula; the cited primary paper recalls this formula in its Introduction, (1.1). VPA determinization is imported from Alur and Madhusudan’s corrected author version. This note’s additional work within the Lab is their explicit composition into an inference procedure, the bound u-l, and the exact one-step scaffold resource contract. This is a reusable sufficient compilation test, not a claim of a new automata class or an established literature novelty.

Residual semantics and graph bisimulation still give different observations: the conclusion is about acceptance under the compiled controller. Neither the reflection estimate nor the cycle test yields arbitrary-context graph equivalence, a pointer-machine lower bound, or a pumping recurrence theorem. The reviewed foundational contracts continue to govern those distinct claims.

Primary sources:

• Nowotka and Srba, Theorem 4, Example 1 and Section 4.1: https://people.cs.aau.dk/~srba/files/NS:MFCS:07.pdf.
• Caucal, author-posted abstract (full construction not inspected): https://www.researchgate.net/publication/221212660_Synchronization_of_Pushdown_Automata.
• Kruk, Lehoczky, Ramanan and Shreve, An Explicit Formula for the Skorokhod Map on [0,a], Introduction (1.1): https://www.math.cmu.edu/users/shreve/DoubleReflection.pdf.
• Alur and Madhusudan, corrected Adding Nesting Structure to Words: https://www.cis.upenn.edu/~alur/Jacm09.pdf.
• Reviewed record compiler and bounded-skew normalization.

7. Evidence and the next bottleneck

The accompanying executable implements finite graph extraction, both cycle tests, bound production and finite observer-table enumeration. It checks positive certificates and the negative controls above; bounded action-word checks compare the reflection formula and estimate against direct clamped updates. Its finite runs do not prove the theorem. It does not implement general pushdown reachability, VPA generation/determinization, the full source-to-scaffold compiler, or a proof assistant.

The next decisive question is whether bottom behavior can be incorporated into a finite inference certificate while retaining a decidable check. The all-pop/all-keep example shows exactly what the current graph forgets. A useful extension must distinguish cycles that can actually run at positive height from cycles confined to bottom; adding more observer states alone cannot repair this failure. Exact fixed-clock, fixed-B verification remains available even when this inference test fails.