{"id":"f3cde739-9ee4-4538-92fb-9d569b746a17","arxiv_id":"1908.02087","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A product construction for Time Petri nets, combined with an extended state class graph algorithm, computes language intersection efficiently without adding expressive power to the model.","lead":"This paper presents a method for computing the common timed action sequences of two Time Petri nets, by joining the two nets into one and building a compact symbolic state graph. The approach is implemented in a tool called Twina and showcased on fault diagnosis and property checking problems.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The LSCG extension for PTPN is stated without a correctness proof, and its firability condition appears to have reversed subscripts, so the algorithm as written may generate an incorrect state class graph.","rationale":"The reader's CONDITIONAL verdict is appropriately cautious: the paper's main contribution, the LSCG construction for PTPN, is asserted without a correctness theorem, and the experimental results do not substitute for soundness. My stress-test sharpens the reader's weakest assumption: not only is the DBM transformation unproven, but the firability condition as written in Section 4 appears to have reversed subscripts, making the described algorithm incorrect on simple domains. This is a genuine correctness risk rather than a stylistic gap. However, the paper does provide an implemented tool, Twina, and several benchmarks; these are useful evidence of practicality, and the error might be a typo in the paper rather than in the implementation. The expressiveness Theorem 2 is restricted to safe, right-closed nets, a limitation acknowledged by the authors, and it is not the load-bearing part for the tool's applicability. Therefore the verdict should remain CONDITIONAL: accept only with a corrected firability condition and a proof of the LSCG extension's exactness, or with evidence that Twina implements the correct condition and preserves the language of the PTPN. My recommendation does not change the reader's verdict, so I mark it UNCHANGED.","tokens_in":14803,"tokens_out":19605,"duration_ms":202086,"concrete_test":"Re-derive the firability condition for a synchronized pair from Definition 5: (ti,tj) is fireable from class (m,D) iff the system D ∪ {x_i=x_j, x_i≤x_k for all k≠i,j} is satisfiable. Apply this exact check and the paper's check to the domain x_i∈[0,1], x_j∈[0,1], x_k∈[2,3]. The exact check accepts, while the paper's condition γ_{t,k}≥0 rejects because γ_{i,k}=−1. This settles that the stated algorithm is incorrect; a corrected condition such as γ_{k,i}≥0 plus equality consistency should be proved and used. As a further check, run Twina's -I option on this example (Figure 1-like nets) and verify whether the successor class after firing (t_i,t_j) is generated; if it is, the tool diverges from the paper's stated condition.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central algorithmic claim of Section 4 is that the three-step DBM transformation for firing a synchronized pair (ti,tj) exactly characterizes the reachable states after that firing. No theorem or proof is provided for this claim, so the correctness of the whole intersection method rests on an unverified procedure. The problem is concrete: the firability test 'γ_{t,k} ≥ 0 for all t∈{i,j} and k enabled' is not the correct condition under the paper's own DBM convention x_i−x_j ≤ γ_{i,j}. To fire ti before tk, one needs a solution with x_i−x_k ≤ 0, i.e., the lower bound −γ_{k,i} of x_i−x_k must be ≤ 0, equivalent to γ_{k,i} ≥ 0, not γ_{i,k} ≥ 0. For example, if the domain contains x_i∈[0,1], x_j∈[0,1], x_k∈[2,3], then γ_{i,k}=−1 and γ_{k,i} could be positive; the paper's test rejects this fireable pair, while the exact check accepts it. Hence the written algorithm under-approximates the reachable classes and can miss valid traces, breaking the claimed language preservation. Even if the implementation uses the correct indices, the paper's exposition does not establish correctness of the LSCG extension.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper proposes a synchronous product construction for Time Petri Nets, called Product TPN (PTPN), whose semantics is designed so that the reachable behavior is isomorphic to the product of the component Timed Transition Systems (Theorem 1). The main algorithmic contribution is an extension of the Linear State Class Graph (LSCG) construction to PTPN, with a three-step DBM transformation for firing a synchronized pair of transitions (Section 4). The paper also claims that PTPN do not add expressive power over TPN for safe, right-closed nets (Theorem 2), and it reports on a tool, Twina, including experiments and applications to twin-plant diagnosability and observer-based verification.","tokens_in":15081,"tokens_out":5868,"duration_ms":59818,"significance":"If the construction is correct, the paper offers a direct and potentially much more efficient route to computing the intersection of TPN languages than existing encodings into timed automata or IPTPN, and the reported experiments show substantial reductions in state class counts compared to the strong SCG on IPTPN. The paper also ships a tool and benchmarks, which is valuable. However, the central algorithmic claim in Section 4 is not backed by a correctness proof, and the stated firability condition appears to have reversed subscripts. The expressiveness result in Section 5 is only sketched. These issues are load-bearing for the paper's main claims, although they seem fixable in a revision.","major_comments":[{"comment":"The firability test stated as 'γ_{t,k} ≥ 0 for all t∈{i,j} and k enabled' uses reversed indices relative to the DBM convention established in the same section, where x_i − x_j ≤ γ_{i,j}. For transition t to be fireable no later than k, one needs a solution with x_t − x_k ≤ 0. The lower bound on x_t − x_k is −γ_{k,t}, so the necessary and sufficient condition with a nonempty DBM is γ_{k,t} ≥ 0, not γ_{t,k} ≥ 0. For example, if the domain contains x_i∈[0,1], x_j∈[0,1], x_k∈[2,3], then γ_{i,k}=−1 and γ_{k,i}=3; the paper's test rejects the fireable pair (t_i,t_k), while the exact check γ_{k,i}≥0 accepts it. Hence the algorithm as written under-approximates the set of reachable classes and can miss valid traces, breaking the claimed language preservation.","section":"Section 4, synchronized firing condition"},{"comment":"No theorem or proof establishes that the three-step DBM transformation for firing a synchronized pair (t_i,t_j) computes the exact set of reachable timed states after that firing, nor that the resulting state class graph preserves the language of the PTPN. The paragraph beginning 'We can draw two useful observations from this result' is not a correctness argument. Since this construction is the central algorithmic contribution and the basis for the intersection computation, a formal correctness statement and proof are required; without it the main claim is unsupported.","section":"Section 4, correctness of the LSCG extension"},{"comment":"The proof of Theorem 2 is only a sketch. The auxiliary properties (L1) and (L2) are stated without proof, and the cited construction T1 from [27] is relied on without stating its exact hypotheses beyond a reference. As Theorem 2 is one of the paper's two main results, the proof needs to be completed or the statement demoted to a conjecture with supporting evidence.","section":"Section 5, Theorem 2"}],"minor_comments":[{"comment":"The phrase 'can leads to' should be 'can lead to'.","section":"Abstract"},{"comment":"The second TTS is written as S2 = (S2, s0_1, →2); the initial state should be s0_2, not s0_1.","section":"Section 2, Definition 2"},{"comment":"The text says 'ratio of classes saved' but the reported percentages appear to be ratios of SSCG classes to LSCG classes; please clarify the exact formula used.","section":"Section 6, Table 1"},{"comment":"The introduction states that the method 'can be applied even when the TPN are not bounded', while the abstract claims efficiency only for bounded nets; please clarify whether boundedness is needed for termination or only for finiteness of the graph.","section":"Introduction and Abstract"},{"comment":"The observation that 'forcing the synchronization of transitions is strictly less constraining than using priorities' is presented as an indirect proof, but no formal comparison with priorities is given; either provide the argument or state it as a conjecture.","section":"Section 4"}],"recommendation":"major_revision","confidential_remarks":"The core idea is promising and the experimental comparison is useful, but the missing correctness proof for the LSCG extension and the index error in the firability condition are the main blockers. I believe a careful revision can address them within the scope of the paper; the result would then be a solid contribution to the timed verification literature."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Worth your time. The genuinely new bit is the Product TPN construction with an LSCG algorithm for synchronized transition pairs, plus the Twina implementation. The benchmark table is credible: their LSCG-based method saves a lot of classes compared to the IPTPN/strong-SCG route, and the applications to twin-plant diagnosability and observer-based checking are sensible. Theorem 1 is essentially a definition check — the semantics is crafted so the isomorphism holds — but that's fine, the math is not circular where it matters. The expressiveness theorem (Theorem 2) uses an existing construction, is honestly limited to safe right-closed nets, and is only sketched, though the sketch is plausible.\n\nNow the soft spots, and the first one is load-bearing. Section 4 gives a three-step DBM transformation for firing a synchronized pair (ti,tj), but no theorem states that this transformation exactly characterizes the reachable states after that firing. For a plain TPN this is classical, but the synchronized case is new and the correctness is asserted, not proven. The stress-test note found something concrete: the firability test says γ_{t,k} ≥ 0 for all t in {i,j} and k enabled. Given the paper's own convention x_i−x_j ≤ γ_{i,j}, to have a solution with x_i ≤ x_k (ti fires before or at tk) you need the lower bound of x_i−x_k to be ≤ 0, which is equivalent to γ_{k,i} ≥ 0, not γ_{i,k} ≥ 0. As written, the test uses the wrong orientation and would reject fireable pairs, under-approximating the reachable class graph and potentially missing valid traces. It may well be a typo, and the implementation might use the correct indices, but the written algorithm is wrong as stated and there is no proof to catch it.\n\nMinor: the abstract overgeneralizes Theorem 2 by saying PTPN \"does not add expressiveness\" without the safe-right-closed caveat that appears in the theorem. Also, the reader's \"circularity\" concern is overstated: the isomorphism is by construction, but the LSCG part and the expressiveness result are not circular.\n\nBottom line: this deserves a real peer review. The construction is useful, the tool is real, and the problem is well-motivated. But the authors need to add a correctness proof for the synchronized LSCG construction and fix the firability condition. If those are addressed, this is a solid contribution.","headline":"The product construction and tool are genuinely useful, but the core state-class correctness claim is unproven and the firability test as written appears to have reversed subscripts.","tokens_in":15628,"tokens_out":2321,"would_cite":true,"duration_ms":22353,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q85","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Firing matching transitions together in a Product TPN makes the state class graph compute the exact language intersection of two Time Petri nets.","keywords":["Time Petri nets","language intersection","state class graph","synchronous product","Arnold-Nivat synchronization","diagnosability","Difference Bound Matrix","timed model checking"],"falsifier":"Enumerate the concrete reachable timed states of a small bounded Product TPN with exact rational arithmetic for all firing schedules up to a fixed depth, then compare the resulting language and markings with the state class graph built by the synchronized-firing rule; any label sequence or marking that appears in one but not the other would refute the method.","tokens_in":14670,"feed_emoji":"⏱️","tokens_out":9409,"duration_ms":107921,"temperature":0.7,"pith_summary":"Two Time Petri nets share a timed trace when they can fire the same labels at the same dates. This paper introduces a product construction, Product TPN, that forces transitions with a common label to fire simultaneously, and proves its semantics is isomorphic to the synchronous product of the component semantics. It then extends the Linear State Class Graph abstraction to such products, so shared timed behavior can be explored symbolically with Difference Bound Matrices. The paper proves the extension adds no expressive power for safe right-closed nets and implements it in a new tool called Twina, with experiments showing the new graph is often much smaller than the previous approach via composable nets.","feed_headline":"One product graph computes the intersection of two Time Petri nets","feed_subtitle":"Matching transitions fire together inside a state class graph, capturing exactly the shared timed traces.","key_machinery":"The central object is the Product TPN, a superposition of two disjoint nets with projections $\\#_1$ and $\\#_2$, equipped with an Arnold-Nivat style synchronization rule. The carrying machinery is the extended Linear State Class Graph: state classes are pairs $(m,D)$ where $D$ is a domain of firing-date constraints represented as a Difference Bound Matrix, a system of bounds $\\alpha_i\\le x_i\\le\\beta_i$ and differences $x_i-x_j\\le\\gamma_{i,j}$ normalized so each solution set has a unique matrix. The new step is the synchronized-firing update, which adds $x_i=x_j$ and $x_i\\le x_k$ before introducing primed variables and eliminating the unprimed ones; this is what lets one class represent all states reachable by firing two transitions at the same date.","core_discovery":"The paper's central claim is that the language intersection of two labelled Time Petri nets can be computed through a product operator, written $N_1\\times N_2$, whose timed transition system $\\llbracket N_1\\times N_2\\rrbracket_\\times$ is isomorphic to the synchronous product $\\llbracket N_1\\rrbracket \\parallel \\llbracket N_2\\rrbracket$ of the component systems (Theorem 1). The product adds one new rule: two transitions from different components that carry the same label and are both time-enabled fire simultaneously; labels not shared, and internal labels, fire asynchronously as in the usual semantics. The algorithmic contribution is an extension of the Linear State Class Graph construction to these synchronized firings: from a class $(m,D)$, firing the pair $(t_i,t_j)$ is computed by adding the constraints $x_i=x_j$ and $x_i\\le x_k$, introducing new variables for the enabled transitions after the firing, and eliminating all old variables, producing a new Difference Bound Matrix. The paper asserts that this procedure gives a DBM characterization of the reachable states after synchronization. It also proves Theorem 2: every safe, right-closed Product TPN is weakly timed bisimilar to a composable TPN of linear size, so the product construction adds no expressive power within that class.","pith_inferences":["If the DBM update is exact, the same equality-based elimination should support synchronizing more than two transitions, giving k-ary products and synchronization vectors with no change to the abstraction; the paper notes this possibility but does not implement it.","A formal correctness proof of the synchronized-firing transformation is the missing piece: without it, the computational results rest on an unproven lemma, and a counterexample would not contradict any theorem in the paper.","The method's practical scalability likely depends on how often matching labels force simultaneous firings; benchmarks with many shared labels and high concurrency would test whether the product graph stays compact.","The quotient (residual) of two TPN languages, the dual of intersection, is a natural next target; a symbolic construction of the same kind would open supervisory control and assume-guarantee reasoning for timed nets."],"forward_implications":["For bounded nets, the state class graph of the product is finite and its language is the intersection of the two component languages, so language intersection is computable without first building each component's full state space.","The twin-plant construction becomes a single product graph: checking diagnosability of a fault reduces to checking that every faulty execution in the product eventually reaches a time deadlock, a property the tool checks on the fly.","A timed property can be expressed as an observer net and checked on the product of the system with the observer, without modifying the system under test.","Because Product TPN add no expressive power for safe right-closed nets, optimization techniques developed for ordinary TPN state classes, such as symmetry reduction, should transfer to the product construction.","In the reported experiments, the linear state class graph of the product is smaller than the strong state class graph of the existing encoding, sometimes by two orders of magnitude."],"supporting_citations":[{"why":"Supplies the Arnold-Nivat synchronization style on which the Product TPN operator is based.","marker":"[3]"},{"why":"Gives the DBM representation and incremental domain update that the synchronized-firing procedure builds on.","marker":"[8]"},{"why":"Introduces the Linear State Class Graph abstraction that the paper extends to Product TPN.","marker":"[9]"},{"why":"Provides the construction that turns a TPN into a composable one, used in the expressiveness theorem.","marker":"[27]"},{"why":"Defines the twin-plant method that motivates the diagnosability application.","marker":"[24]"},{"why":"Provides the reference implementation and net syntax used for the experimental comparison via the composable-net encoding.","marker":"[12]"}],"fun_headline_variants":["Pairing matching labels in state classes computes TPN language intersection","Product graph with synchronized firing captures exact shared timed traces","One DBM extension gives the common language of two Time Petri nets","Twina tool builds a product net to compute TPN language intersection","New product rule for time-enabled transitions yields intersection language"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the symbolic update for firing two synchronized transitions together exactly characterizes the reachable states after that firing, with no loss and no extra states; the paper uses this update to compute the graph but does not prove a correctness theorem for it.","fun_headline_variants_meta":{"raw":{"variants":["Pairing matching labels in state classes computes TPN language intersection","Product graph with synchronized firing captures exact shared timed traces","One DBM extension gives the common language of two Time Petri nets","Twina tool builds a product net to compute TPN language intersection","New product rule for time-enabled transitions yields intersection language"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000239,"raw_usage":{"total_tokens":1518,"prompt_tokens":950,"completion_tokens":568,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":566,"completion_tokens_details":{"reasoning_tokens":494}},"tokens_in":566,"tokens_out":568,"duration_ms":6779,"temperature":1.0,"reasoning_tokens":494,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:53:45.802941+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Enumerate the concrete reachable timed states of a small bounded Product TPN with exact rational arithmetic for all firing schedules up to a fixed depth, then compare the resulting language and markings with the state class graph built by the synchronized-firing rule; any label sequence or marking that appears in one but not the other would refute the method.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies the Arnold-Nivat synchronization style on which the Product TPN operator is based."},{"cited_title":"In: Proceedings IFIP (1983)","cited_arxiv_id":null,"evidence_quote":"Introduces the Linear State Class Graph abstraction that the paper extends to Product TPN."},{"cited_title":"IEEE Transactions on Automatic Control 46(8) (2001)","cited_arxiv_id":null,"evidence_quote":"Defines the twin-plant method that motivates the diagnosability application."},{"cited_title":"International Journal of Production Research 42(14) (2004)","cited_arxiv_id":null,"evidence_quote":"Provides the reference implementation and net syntax used for the experimental comparison via the composable-net encoding."}],"review_version":1}