{"id":"126ec7d6-eb7b-4569-b8bc-bc8d93e68d9e","arxiv_id":"2607.13981","paper_version":1,"verdict":"ACCEPT","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Model checking the agent-alternation-free fragment of epistemic metric temporal logic with past is EXPSPACE-complete, with hardness already at one agent, one knowledge operator, and only the unbounded interval.","lead":"This paper defines an epistemic metric temporal logic with past (KMTL) and shows that model checking its agent-alternation-free fragment over Büchi automata under synchronous perfect recall is EXPSPACE-complete. The result pinpoints the exact complexity of a logic motivated by diagnosis and opacity, where past operators plus a single knowledge operator already force exponential-space hardness.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"No significant objection identified","rationale":"The reader correctly identifies the pointed-tester lemma (Lemma 34/16) as the most load-bearing and delicate part of the upper-bound proof. My review focused on exactly this lemma, checking the counter recurrences, the Büchi conditions, and the induction for both future and past schemes. I also examined the observer construction for knowledge and the lower-bound reduction. In each case, the argument holds: cheating runs are excluded by the recurrence and acceptance conditions, and the recursive liveness predicates are well-founded. No alternative concern—such as complexity blow-up beyond EXPSPACE or a flaw in the tiling reduction—appeared more serious. Hence I agree with the reader's identification of the weakest assumption, but I do not find that it actually fails; the correctness risk remains at 'medium' rather than 'high,' and the ACCEPT verdict is appropriate. A targeted computational test of the lemma on small formulas would be a useful independent check, but it is not required to flag a specific defect.","tokens_in":23076,"tokens_out":27349,"duration_ms":259144,"concrete_test":"Implement the pointed-tester construction of Definition 33 for a small knowledge-free formula combining a future lower-bound scheme and a past scheme, e.g., θ = ♢p ∧ ♢⁻q, and exhaustively verify the equivalence in Lemma 16(ii) over all ultimately periodic words of period ≤ 4 and length ≤ 8. Any mismatch between w,i ⊨ θ and the existence of an accepting run of A_θ with a marked state at position i would indicate a flaw in the upper bound; a clean pass would corroborate the proof.","verdict_should_be":"UNCHANGED","load_bearing_attack":"I examined the upper-bound construction in detail, especially Lemma 34/16 (the pointed Büchi testers for the knowledge-free fragment), the observer/liveness recursion for KMTL1, and the lower-bound tiling reduction. The proof of Lemma 34 is delicate but internally consistent: the backward-propagated future counters and forward-propagated past counters are tightly constrained by the recurrence in Definition 32, and the Büchi conditions for lower-bound future schemes do rule out cheating runs that would leave an obligation unfulfilled. The induction establishing the pointed property handles the no-witness case by forcing the counter to ⊥, which is consistent with the recurrence and the acceptance condition. The observer construction also appears well-founded: the relative-liveness predicate is defined by recursion on knowledge depth, and the update order (innermost-outward) correctly feeds the semantic values of inner knowledge formulas to the counterexample automaton. The lower bound is likewise sound: the hidden-tag argument gives the knowledge formula the required universal quantification over vertical edges, and the model has polynomial explicit size. I found no concrete gap, circular step, or unjustified assumption that would undermine the central EXPSPACE-completeness claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper defines KMTL, an epistemic metric temporal logic with future and past operators, strict first-time semantics, binary-encoded metric intervals, and synchronous perfect-recall knowledge over Büchi automata, and studies the agent-alternation-free fragment KMTL1. The main result is that universal model checking for KMTL1 is EXPSPACE-complete. The lower bound is a reduction from exponential-width corridor tiling; the constructed formula uses one agent, one occurrence of the knowledge operator, and only the unbounded interval N, with all past operators inside the knowledge operator. The upper bound combines exponential-size pointed Büchi testers for the knowledge-free fragment with perfect-recall observers that track pairs of system states and tester states, and introduces a recursive 'relative liveness' predicate to handle nested same-agent knowledge under future operators. The paper also formalizes centralized diagnosis, decentralized diagnosis, and opacity in KMTL1.","tokens_in":23339,"tokens_out":29579,"duration_ms":298295,"significance":"If the proof is correct, the paper gives a clean complexity boundary: adding past to the PSPACE-complete future-only epistemic fragment yields EXPSPACE-completeness even with trivial metric bounds, while the knowledge-free strict-first-time metric fragment remains PSPACE. The lower bound is a careful adaptation of the forgettable-past tiling reduction, and the upper-bound observer construction—using product states (system state, temporal tester state) rather than bare information sets—is a substantive technical contribution. The appendix is detailed and self-contained; the reduction is from a known EXPSPACE-complete problem, and the upper bound provides constructive automata with polynomial-space testable local predicates. The delicate pointed-tester lemma (Lemma 34 / Appendix B.1) withstands scrutiny: the recurrence for future counters and the Büchi conditions rule out cheating runs, while past counters are anchored by the initial position. The diagnosis/opacity encodings are a useful sanity check and fit the fragment.","major_comments":[],"minor_comments":[{"comment":"The soundness proof compresses the 'no witness' case. It would aid the reader to spell out explicitly why an accepting run cannot carry non-truthful finite future counters: an upper-bound counter would have to decrease indefinitely, and a saturated lower-bound counter would violate the generalized Büchi condition Gγ. This is implicit in the current text but central to the pointed-tester property.","section":"Lemma 34 / Appendix B.1"},{"comment":"The relative-liveness update post(I,o) is described as updating components 'from the deepest blocks outward.' Since correctness of an outer tester depends on this update order, a recursive formal definition or pseudocode would remove ambiguity.","section":"Definition 36 / Appendix B.2"},{"comment":"The table attributes the PSPACE model-checking upper bound for the knowledge-free metric fragment to [1], but the cited paper is primarily about satisfiability. Please state explicitly that the model-checking bound follows by the standard product construction, or cite a source that proves it.","section":"Table 1 / Section 1"},{"comment":"The proof uses monotonicity of Ka♢−f (the alarm persists once true). A one-line justification under perfect recall—extending an observation prefix preserves the existence of a fault in every compatible prefix—would make the argument fully self-contained.","section":"Lemma 8"},{"comment":"When presenting the normal-form splitting of intervals, it may help to note explicitly that the two conjuncts refer to the same first-witness distance; this is exactly why the equivalence holds under strict first-time semantics.","section":"Section 2, Definition 28"}],"recommendation":"accept","confidential_remarks":"I found no load-bearing technical flaw. The main EXPSPACE-completeness claim is well supported by the appendix, and the delicate points identified in the stress test—the pointed-tester lemma and the observer/liveness recursion—are internally consistent. The minor comments are presentation and clarity requests only; they do not affect the verdict."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Bottom line: this gives the exact model-checking complexity for the shallow epistemic metric temporal logic with past, and the result is EXPSPACE-complete. The lower bound is strong—one agent, one K, unbounded interval only—so the hardness comes from combining past with knowledge, not from metric constants. The upper bound is the real work, and it holds up on inspection.\n\nWhat is actually new is the logic KMTL1 and its complexity. The lower-bound reduction adapts the forgettable-past tiling construction with a clever hidden-tag mechanism; the upper bound extends the strict-first-time test automata to past operators and adds observers over (system state, tester state) pairs. The paper is self-contained, with detailed appendix proofs, and I found no circular reasoning or suspicious citation patterns.\n\nThe delicate point is Lemma 16/34, the pointed Büchi tester for the knowledge-free fragment. I went through the recurrence for counters and the Büchi condition for lower-bound future schemes. The construction is consistent: the counters are tightly constrained, and the generalized Büchi condition does rule out runs that leave an obligation active forever. The induction establishing the pointed property handles the no-witness case by forcing the counter to bottom, which works. This is exactly the kind of lemma that should be checked by a second pair of eyes, but I did not find a concrete gap.\n\nOne soft spot worth raising in review: the lower-bound model Mtag_T is defined by a regular language, and the authors say it has polynomial size because each state only admits O(|T|) output letters. That is reasonable only if the input model is allowed to be succinctly represented, since the alphabet is 2^APT, exponential in the instance. The paper never states the input encoding for Büchi automata. If the community standard requires an explicit transition table, the reduction would need elaboration. I assume symbolic transitions are allowed, but the definition should say so.\n\nMinor point: the diagnosis/opacity encodings are correct but standard; they serve as motivation, not as new technical content.\n\nWho is this for: anyone working on epistemic temporal logics, metric temporal logic, or diagnosability/opacity in discrete-event systems. It deserves a serious referee and, after minor revision, acceptance. I would bring it to reading group and cite it.","headline":"Closes a natural open complexity question with a well-engineered EXPSPACE-completeness proof; the hard part is the upper bound, which looks sound, though the lower bound's model encoding should be stated explicitly.","tokens_in":23790,"tokens_out":5262,"would_cite":true,"duration_ms":57231,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B44","03B70","68Q17","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper establishes that model checking KMTL1, the agent-alternation-free fragment of epistemic metric temporal logic with past, is EXPSPACE-complete—lower bound with one agent and one knowledge operator, upper bound via temporal test aut","keywords":["epistemic temporal logic","metric temporal logic","past operators","synchronous perfect recall","model checking","Büchi automata","EXPSPACE-complete","diagnosability and opacity"],"falsifier":"Build A_θ for θ = (p U^1_{≥2} q) and run it on the infinite word p p p r r r ... where q never occurs. Strict-first-time semantics makes θ false at every position, so no accepting run may ever enter a marked state. If the constructed round-robin Büchi automaton admits an accepting run with a marked state, the generalized Büchi set G_γ has failed to rule out a saturated lower-bound counter that never reaches a witness, and Lemma 34 (hence the EXPSPACE upper bound) is false.","tokens_in":23014,"feed_emoji":"⏳","tokens_out":8243,"duration_ms":85317,"temperature":0.7,"pith_summary":"The paper studies KMTL1, the fragment of epistemic metric temporal logic with past in which nested knowledge operators always refer to the same agent. Its central claim is that model checking KMTL1 over Büchi automata under synchronous perfect recall is EXPSPACE-complete. This matters because the intended applications—centralized diagnosis, decentralized diagnosis, and opacity—are stated naturally in this fragment. The lower bound is sharp: EXPSPACE-hardness already appears with one agent, one occurrence of the knowledge operator, and no nontrivial metric bounds. The matching upper bound combines exponential-size pointed automata for knowledge-free formulas with perfect-recall observers that record pairs of system state and automaton state, because past formulas can disagree on indistinguishable histories ending in the same state.","feed_headline":"Past plus knowledge makes model checking EXPSPACE-complete","feed_subtitle":"Adding a single knowledge operator and past operators to metric temporal logic jumps complexity to full exponential space.","key_machinery":"The load-bearing construction is the pointed Büchi tester A_θ: for every knowledge-free θ it is an exponential-size automaton whose states are temporal types storing one counter per metric scheme, and whose marked states C_θ satisfy w,i |= θ exactly when some accepting run is marked at position i. Past-scheme counters are computed forward from the initial position; future-scheme counters are guessed backward from a witness, and a generalized Büchi condition rejects runs that keep a lower-bound obligation active forever without ever reaching its witness. Around this tester, the model-checking algorithm builds perfect-recall observers: for each knowledge block K_a ψ it maintains the set of pai","core_discovery":"The central discovery is the exact complexity: KMTL1 model checking over Büchi automata is EXPSPACE-complete. The lower-bound reduction from exponential-width corridor tiling produces a polynomial-size tagged automaton in which all states are accepting, and a formula with one agent, one knowledge operator, and only the unbounded interval N=[0,∞). The knowledge operator quantifies over hidden tag placements to check vertical tile compatibility, so metric constants are not the source of hardness. The upper bound shows that the truth of a knowledge-free formula can be captured by a Büchi automaton of exponential size whose states carry one counter per metric scheme, with past counters propagate","pith_inferences":["Beyond the paper: the same observer construction—products of model states with tester states plus relative liveness—should transfer to other ω-automaton acceptance conditions, with only the liveness projection changing, so the EXPSPACE upper bound is a plausible template.","Beyond the paper: the lower-bound trick of using knowledge to quantify over hidden tags that select distant grid cells suggests a general way to simulate random access without metric constants; it might apply to satisfiability or synthesis questions for related shallow epistemic fragments.","Beyond the paper: the paper leaves open the exact complexity for standard metric semantics, conjecturing 2-EXPSPACE-completeness; a concrete next step is to test whether a double-exponential counter hierarchy can be simulated by nesting the present tester construction with binary metric constants.","Beyond the paper: discrete-time monitorability is stated as open; the relative-liveness graph introduced here may be adaptable to decide whether every observation prefix can be extended to a definitive verdict, possibly with the same EXPSPACE boundary."],"forward_implications":["Deciding whether all accepted words of a Büchi automaton satisfy a KMTL1 formula can be done in deterministic exponential space, and no polynomial-space decision procedure can exist unless the standard complexity classes collapse.","The EXPSPACE lower bound is achieved with one agent, one knowledge operator, and only the unbounded interval; even this minimal slice of the logic is already as hard as full exponential space.","Bounded centralized diagnosis, decentralized codiagnosability, and past-event opacity are expressible in KMTL1, so each of these observation-based verification problems inherits the EXPSPACE-complete bound when the system is given by a Büchi automaton.","For formulas with past, an information set over system states is insufficient: the observer must carry a temporal automaton state for each system state, because past formulas can have different truth values on indistinguishable histories.","The complexity boundary is tight along this axis: the metric-free epistemic fragment with future operators is PSPACE-complete at alternation depth one, while adding past operators jumps the problem to EXPSPACE-complete."],"fun_headline_variants":["Agent-alternation-free KMTL model checking is EXPSPACE-complete","One knowledge operator makes model checking EXPSPACE-complete","EXPSPACE-complete: even a single knowledge operator is hard","Past formulas plus one knowledge operator: EXPSPACE-hard","Exact complexity: KMTL1 model checking is EXPSPACE-complete"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The EXPSPACE upper bound rests on the tester lemma: for every knowledge-free formula θ, the constructed automaton A_θ marks exactly the positions where θ holds, with all local predicates testable in polynomial space; if the backward-guessed future counters and forward-propagated past counters can drift from strict-first-time witness distances on some word, the upper-bound construction collapses.","fun_headline_variants_meta":{"raw":{"variants":["Agent-alternation-free KMTL model checking is EXPSPACE-complete","One knowledge operator makes model checking EXPSPACE-complete","EXPSPACE-complete: even a single knowledge operator is hard","Past formulas plus one knowledge operator: EXPSPACE-hard","Exact complexity: KMTL1 model checking is EXPSPACE-complete"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000272,"raw_usage":{"total_tokens":1438,"prompt_tokens":681,"completion_tokens":757,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":425,"completion_tokens_details":{"reasoning_tokens":659}},"tokens_in":425,"tokens_out":757,"duration_ms":6673,"temperature":1.0,"reasoning_tokens":659,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T03:07:50.022826+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build A_θ for θ = (p U^1_{≥2} q) and run it on the infinite word p p p r r r ... where q never occurs. Strict-first-time semantics makes θ false at every position, so no accepting run may ever enter a marked state. If the constructed round-robin Büchi automaton admits an accepting run with a marked state, the generalized Büchi set G_γ has failed to rule out a saturated lower-bound counter that never reaches a witness, and Lemma 34 (hence the EXPSPACE upper bound) is false.","supporting_citations":[],"review_version":1}