{"id":"25f185fd-2088-482a-a08c-a4414be93365","arxiv_id":"2505.12107","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":3,"one_line_summary":"The authors introduce PriTL, an algorithm that infers concise PLTL formulas separating positive from negative Markov chains, with soundness proofs and demonstrations on RL policies and protocol variants.","lead":"A new tool, PriTL, learns readable probabilistic temporal logic rules that separate good stochastic behaviors from bad ones, such as policies from reinforcement learning. If it works, engineers can automatically obtain logical explanations for why one policy or protocol variant differs from another.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"The bounded Boolean set-cover step (Algorithm 3, line 5) is not proved to preserve completeness or minimality, so Theorem 1's minimal-PLTL+ claim overreaches.","rationale":"The reader's weakest assumption identifies the same load-bearing step: BSC's bounded, score-based candidate selection is used in the minimality proof without a completeness argument. My read of the algorithm and Theorem 1 confirms that this is not a cosmetic gap. Soundness (Lemmas 2 and 4) is argued credibly, the GBE enumeration lemma is plausible, and the experiments show a working tool, so the paper deserves a conditional rather than outright rejection. But the proof of Theorem 1's second bullet jumps from GBE exhaustiveness and Lemma 3 to minimality, silently bypassing Algorithm 3's truncation to the L best candidates and its single-pass binary combination loop. Since PLTL+ formulas are produced only by BSC, the theorem's central novelty (exact minimal PLTL+ learning) is not established. The suggested exhaustive-mode comparison is a concrete way to see whether the truncation actually loses minimal formulas in practice or only in principle. If the exhaustive mode never finds smaller formulas on the tested samples, the concern would be weakened empirically, though a proof would still be needed for the universal claim. I therefore keep the reader's CONDITIONAL verdict unchanged and recommend the authors either prove a completeness property for BSC under the stated limits or weaken Theorem 1 to minimality among PLTL formulas found by PTS.","tokens_in":16857,"tokens_out":11880,"duration_ms":131613,"concrete_test":"Run PriTL in two configurations on the published benchmarks plus a hand-built sample: (1) published mode with L=10; (2) an exhaustive BSC mode with L=|Bn| and repeated closure under conjunction/disjunction up to size K. For the hand-built sample, use two positive DTMCs where atoms A and B each hold almost surely, and two negative DTMCs where A holds in one and B in the other, so the minimal PLTL+ formula is A and B but neither A nor B alone has a top-L score. If configuration (2) returns a strictly smaller consistent formula than configuration (1), or returns one where (1) fails, then Algorithm 3 line 5 breaks the minimality claim of Theorem 1 as stated.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 1's completeness-and-minimality clause asserts that, whenever a PLTL formula in Theta(K,D,delta) is consistent with S, the algorithm returns a minimal PLTL+ formula. The proof cites exhaustive GBE (Lemma 1) and Lemma 3, but the returned formula can be built by BSC (Algorithm 3), and BSC is not exhaustive. Algorithm 3 line 5 retains only the L highest-scoring PLTL candidates in H*, and line 6 forms only binary combinations Psi o Phi with Psi in H and Phi in H*, without adding new combinations back into H. No lemma states that every atom of a minimal PLTL+ formula lies in H*, nor that a Boolean combination requiring more than one pairwise step can be constructed. A formula useful only inside a conjunction can have a low individual score because it is true in some negative examples, reducing c(phi,r), so it may be excluded from H* and the minimal combination is never considered. L itself does not appear in the statement or proof of Theorem 1, yet correctness would have to depend on it. Lemma 4 proves only soundness of formulas BSC returns, not completeness or minimality. The central guarantee therefore lacks a proof for exactly the step that produces PLTL+ formulas.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper addresses the passive learning problem of inferring probabilistic linear temporal logic (PLTL) specifications over finite Markov chains. The input is a sample of positive and negative DTMCs, and the goal is a concise PLTL+ formula (a positive Boolean combination of PLTL formulas) that is satisfied by all positive examples and violated by all negative examples. The proposed algorithm, PriTL, combines three procedures: grammar-based enumeration (GBE) of LTL formulas, probabilistic threshold search (PTS) that uses probabilistic model checking to choose probability thresholds, and a Boolean set cover (BSC) procedure that forms Boolean combinations of PLTL candidates. The paper states a soundness, completeness, and minimality guarantee (Theorem 1) and evaluates the tool on RL policy DTMCs and on variants of the EGL contract-signing protocol. The empirical results show that the method finds concise distinguishing formulas in both case studies.","tokens_in":17102,"tokens_out":10444,"duration_ms":110760,"significance":"If the stated guarantees held, this would be the first exact passive learner for probabilistic temporal logic specifications over Markov chains, and the combination of grammar-based enumeration with off-the-shelf probabilistic model checking is a natural and potentially reusable design. The soundness arguments for PTS (Lemma 2) and for the formulas output by BSC (Lemma 4) are credible, and the two case studies demonstrate practical value: the method recovers interpretable formulas that separate RL strategies and detects the absence of distinguishing formulas in the EGL variant comparison. The paper also provides a prototype tool and reproducible experimental setup. However, the completeness-and-minimality claim in Theorem 1 substantially overreaches what is proved: the bounded, score-based BSC step is not shown to preserve completeness or minimality, and the proof of Lemma 1 requires a completeness property of the temporal simplification rules that is not established. These gaps directly affect the paper's central theoretical contribution.","major_comments":[{"comment":"The completeness and minimality clause of Theorem 1 is not justified by the proof. Algorithm 3 line 5 retains only the L highest-scoring PLTL formulas in H*, and line 6 forms only binary combinations Ψ∘Φ with Ψ∈H and Φ∈H*, without adding new combinations back into H; moreover, BSC is invoked on Bn, the formulas of the current size n, so it never combines PLTL atoms of different sizes. No lemma states that every atom of a minimal PLTL+ formula lies in H*, nor that a Boolean combination with more than one Boolean operator or with unequally sized atoms can be constructed. A component formula can be individually low-scoring because it is true in some negative examples, reducing c(φ,r), and can therefore be excluded from H*, after which the minimal combination containing it is never considered. The parameter L does not appear in the statement or proof of Theorem 1, yet the claimed guarantee would have to depend on it. Consequently, even a minimal PLTL+ formula of the form P>p[a] ∧ P>q[G F b], with atoms of sizes 1 and 3, cannot be produced by the algorithm as written, since no iteration of BSC combines size-1 with size-3 candidates.","section":"§4.3, Algorithm 3, Theorem 1"},{"comment":"The proof of Lemma 1 is incomplete. It claims that GBE discards a formula ψ only if there exists an already-enumerated ψ' with ψ≡ψ', but the temporal simplification heuristic actually discards any formula that is not in the syntactic normal form produced by the rewrite rules. The paper does not prove that these rewrite rules are complete for semantic equivalence over (2^AP)^ω, i.e., that every discarded formula is semantically equivalent to a smaller formula already generated. The Boolean simplification heuristic does include a semantic equivalence check via LTL satisfiability, but the temporal simplification does not. Therefore a semantically new formula of size ≤N' and depth ≤D can be discarded, breaking the exhaustive-enumeration premise on which Theorem 1's completeness argument rests.","section":"§4.1 and Appendix A, Lemma 1"},{"comment":"The pruning rule in PTS discards φ when VM,φ≡0 for each M∈P or VM,φ≡1 for each M∈N, but Lemma 3 proves only the positive case. The text says 'a similar argument applies to the negative cases' without giving the proof. The negative case is not immediately symmetric: a formula that is true in every negative example can still be useful as a conjunct of a conjunction whose truth on negatives is decided by the other conjunct. A rigorous dual argument is needed to justify discarding formulas in this case, and it should be stated explicitly because the completeness guarantee depends on not discarding useful subformulas.","section":"§4.2, Lemma 3"}],"minor_comments":[{"comment":"The definition of |Φ| for PLTL+ formulas says it is defined 'exactly the same way' as the LTL size, but it is unclear whether the probability threshold p and the P operator are counted; please clarify, since the threshold values affect the statement of the size bound K in Problem 1.","section":"§2.2"},{"comment":"There is an inconsistency in the name of the Q-learning variant used for suboptimal strategies: the main text refers to the 'KC' algorithm, while Appendix C.1 uses 'CF' in one place and 'KC' in the next; please make the naming consistent.","section":"§5 and Appendix C.1"},{"comment":"The high-level flow suggests that at each size n, PTS and BSC both run before moving to n+1, but Algorithm 2 has an early return. Please state explicitly whether BSC is skipped when PTS finds a consistent PLTL formula, as this affects the minimality claim.","section":"Figure 2 and §4"},{"comment":"The column 'LTL Searched' reports fractions such as 24/24 and 110/186; the denominator is not defined in the text or caption, so it is unclear whether it counts all formulas up to the learned formula's size, before or after heuristics.","section":"Table 1"},{"comment":"The sentence 'Based on the semantics of X, π[1:] |= φ for some i∈N' is garbled: the semantics of X involves π[1:], with no index i, whereas the index i belongs to the F or U cases. Please correct this typo.","section":"Appendix A, proof of Lemma 3"},{"comment":"Reference [Brockman, 2016] duplicates [Brockman et al., 2016] and should be merged or removed.","section":"References"}],"recommendation":"major_revision","confidential_remarks":"The empirical results and the soundness lemmas are credible and the tool is a useful contribution, but the advertised completeness-and-minimality guarantee is the main selling point of the paper and it is not supported by the algorithm as presented. The major issues are (i) BSC's bounded, score-based selection and its single-pass binary combination scheme cannot establish the claimed PLTL+ minimality, and (ii) Lemma 1's proof assumes a completeness property of temporal simplification that is not proved. These are fixable by either strengthening the analysis (e.g., proving that the scoring cut preserves the needed candidates, or restricting the theorem to the actually searched space) or by substantially weakening Theorem 1 to a soundness-with-heuristics statement. Given the journal context, I think the appropriate decision is major revision rather than rejection, because the core algorithmic idea and the experiments are valuable and the theoretical overreach is localized to the theorem and the BSC/GBE analysis."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"PriTL is a real tool that learns probabilistic temporal logic formulas from positive and negative Markov chains, and the case studies are convincing. The problem formulation is new as far as I know, and the pipeline — grammar enumeration, probability-vector computation via PRISM, threshold search, then Boolean combination — makes sense. The soundness results (Lemma 2, Lemma 4) are simple and credible. The paper deserves serious referee attention. But the main theorem overreaches, exactly as the stress-test says.\n\nThe completeness-and-minimality clause in Theorem 1 is not proved. BSC (Algorithm 3) keeps only the L highest-scoring candidate formulas in H*, makes one round of binary combinations, and never adds new combinations back into H. Any minimal PLTL+ formula that needs a conjunction of three atoms, or an atom that is individually low-scoring because it is true in some negative examples, can be missed. L appears nowhere in Theorem 1. Also, as far as I can tell from Algorithm 3, BSC only combines formulas from the current size bucket Bn, so it cannot combine a size-2 atom with a size-3 atom even with unlimited L. The proof of Theorem 1 cites GBE exhaustiveness and Lemma 3, but neither covers the bounded, score-based BSC step.\n\nThere is a second, smaller gap. Lemma 1's proof in Appendix A states that GBE discards a formula only if it is semantically equivalent to a smaller one, but the actual heuristics are specific rewrite rules. Those rules are sound, but they are not shown to catch every semantic equivalence. The lemma may still hold, but the proof as written isn't complete.\n\nNone of this makes the paper useless. The tool finds the expected formulas in the experiments; the EGL case where no formula exists is a nice touch. The fix is straightforward in spirit: either prove a completeness property for BSC under the stated bounds (I suspect it's false), or weaken Theorem 1 to soundness plus completeness for single PLTL formulas found by PTS, and describe BSC as a heuristic that returns consistent (but not necessarily minimal) PLTL+ formulas. That is an honest and still interesting claim.\n\nI'd send this to a competent reviewer. The paper is for researchers in specification mining and explainable RL. I would cite the tool and problem formulation, but not the minimality theorem.","headline":"Solid tool paper with a real new problem formulation, but Theorem 1's minimality claim is not supported by the bounded Boolean set-cover step; the fix is to weaken the theorem.","tokens_in":17608,"tokens_out":6713,"would_cite":true,"duration_ms":69897,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"Passive learning of probabilistic temporal logic specifications is solved exactly: the proposed algorithm returns a minimal consistent PLTL+ formula whenever a bounded PLTL formula exists.","keywords":["probabilistic linear temporal logic","specification learning","Markov chains","passive learning","grammar-based enumeration","probabilistic model checking","Boolean set cover","reinforcement learning"],"falsifier":"Construct a sample of positive and negative DTMCs whose unique minimal consistent PLTL+ formula is $\\Phi_1 \\wedge \\Phi_2$, with each component's score below the $L$-th best candidate and each component individually not consistent with the sample; run the algorithm with $K = |\\Phi_1 \\wedge \\Phi_2|$, the chosen depth $D$, and the chosen $\\delta$. If the output is not $\\Phi_1 \\wedge \\Phi_2$ or is a larger formula, the completeness-and-minimality claim is false for the implemented algorithm.","tokens_in":16648,"feed_emoji":"🎲","tokens_out":12293,"duration_ms":115326,"temperature":0.7,"pith_summary":"This paper tackles the passive-learning problem for stochastic systems: from a set of Markov chains labeled positive or negative, learn a concise specification in probabilistic linear temporal logic (PLTL+) that all positive examples satisfy and no negative example satisfies. The paper proposes a three-stage algorithm that enumerates LTL formulas by size and nesting depth, computes probabilistic satisfaction thresholds for each candidate by model checking, and combines surviving candidates into Boolean formulas via a set-cover step. If a PLTL formula of bounded size, depth, and probability gap separates the sample, the algorithm is claimed to return a smallest consistent PLTL+ formula; if no such formula exists, it reports none. The motivation is that such specifications explain stochastic behaviour, for example the difference between reinforcement-learning policies or between variants of a probabilistic protocol.","feed_headline":"First exact learner turns Markov chains into probabilistic LTL","feed_subtitle":"Positive and negative Markov chains become concise PLTL+ formulas, with proof of minimality within bounded search.","key_machinery":"The load-bearing object is a PLTL+ formula: a positive Boolean combination, using conjunction and disjunction, of probabilistic LTL statements of the form $P_{\\triangleright\\triangleleft p}[\\varphi]$, each asserting that the probability of an LTL formula $\\varphi$ holding along paths of the DTMC meets threshold $p$. The argument is carried by three procedures over candidate LTL formulas: grammar-based enumeration generates all semantically distinct formulas up to size and nesting depth; probabilistic threshold search computes the probability vector for each candidate on every sample DTMC, reads off the minimum probability among positive examples and the maximum among negative examples, and when the gap exceeds tolerance $\\delta$ emits the PLTL formula whose threshold is the midpoint of that gap; Boolean set cover scores leftover candidates by how many sample DTMCs they separate and combines the top $L$ into conjunctions and disjunctions. The midpoint threshold is what converts a measured probability gap into a classifier that every positive example satisfies and no negative example satisfies.","core_discovery":"The central discovery is that exact passive learning transfers from deterministic traces to stochastic models by replacing trajectory satisfaction with model-checked satisfaction probabilities and by letting Boolean combinations absorb cases where no single PLTL formula separates the classes. Concretely, the paper claims Theorem 1: with sample size $|S|$, size bound $K$, depth bound $D$, and tolerance $\\delta$, the learning algorithm is sound (every returned PLTL+ formula is consistent with the sample and has size at most $K$) and complete-and-minimal (if there exists a PLTL formula in the bounded search space $\\Theta(K,D,\\delta)$ consistent with the sample, it returns a minimal PLTL+ formula). The proof rests on exhaustive grammar-based enumeration, sound threshold search, and the observation that formulas unsatisfiable in every positive state cannot occur in a minimal consistent formula.","pith_inferences":["The published algorithm's Boolean set-cover stage keeps only the $L$ highest-scoring candidates; the proof of Theorem 1 does not address this truncation, so in practice exact minimality of PLTL+ formulas should be read as guaranteed only for the single-formula PLTL case or when the optimal combination lies within the retained shortlist.","The same framework could be re-instantiated with a different model-checking oracle, for example one that computes expected rewards, to learn specifications with quantitative reward objectives instead of path probabilities.","The midpoint-threshold rule suggests a natural active-learning extension: ask a teacher to label the examples whose measured probabilities fall in the ambiguous gap between the worst positive and best negative values, using the algorithm's own scores to select the most informative queries."],"forward_implications":["For any finite sample of Markov chains, the bounded learning problem becomes decidable: the algorithm terminates and either returns a consistent formula of size at most $K$ or certifies that no bounded consistent PLTL formula exists.","The learned formulas are small enough to serve as explanations; in the experiments, distinctions between policies trained for different LTL tasks are recovered as statements such as a high probability of globally avoiding holes or of repeatedly reaching a target.","A negative result is also informative: for the protocol with more than five secrets, the exhaustive search shows that no formula of the chosen size and depth separates the variants, so the variants are indistinguishable at that specification budget.","The tolerance parameter $\\delta$ makes the learned descriptions insensitive to small probability perturbations, so the specifications do not chase noise in the sample probabilities."],"supporting_citations":[{"why":"Supplies the standard probabilistic LTL model-checking construction used by PTS to compute satisfaction probabilities, as well as LTL simplification rules used by GBE.","marker":"[Baier and Katoen, 2008]"},{"why":"Supplies the model checker used to evaluate candidate LTL formulas on the sample DTMCs and extract the probability vectors in PTS.","marker":"[Kwiatkowska et al., 2011]"},{"why":"Supplies the Boolean set-cover procedure and scoring function that BSC adapts to probabilistic thresholds.","marker":"[Raha et al., 2022]"},{"why":"Supplies LTL simplification and satisfiability checking behind the temporal and Boolean simplification heuristics that make GBE complete while pruning.","marker":"[Duret-Lutz et al., 2022]"},{"why":"Supplies the reinforcement-learning algorithms used to generate the strategy DTMCs in the first case study.","marker":"[Shao and Kwiatkowska, 2023]"},{"why":"Supplies the EGL protocol variants used as the second case study.","marker":"[Norman and Shmatikov, 2006]"}],"fun_headline_variants":["Exact PLTL learner for stochastic systems from Markov chains","Learning temporal logic specs from positive/negative Markov chains","Passive learning of probabilistic LTL from classified Markov chains","Inferring concise PLTL formulas from Markov chain examples","Exact minimal PLTL+ formulas from positive and negative chains"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the Boolean set-cover step keeps enough candidate formulas when it truncates to the L highest-scoring ones; the paper gives no proof that a minimal consistent PLTL+ combination can always be built from that shortlist, so if the needed formula is discarded the completeness-and-minimality guarantee fails.","fun_headline_variants_meta":{"raw":{"variants":["Exact PLTL learner for stochastic systems from Markov chains","Learning temporal logic specs from positive/negative Markov chains","Passive learning of probabilistic LTL from classified Markov chains","Inferring concise PLTL formulas from Markov chain examples","Exact minimal PLTL+ formulas from positive and negative chains"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000722,"raw_usage":{"total_tokens":3195,"prompt_tokens":854,"completion_tokens":2341,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":470,"completion_tokens_details":{"reasoning_tokens":2260}},"tokens_in":470,"tokens_out":2341,"duration_ms":16427,"temperature":1.0,"reasoning_tokens":2260,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-15T20:41:54.744683+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Construct a sample of positive and negative DTMCs whose unique minimal consistent PLTL+ formula is $\\Phi_1 \\wedge \\Phi_2$, with each component's score below the $L$-th best candidate and each component individually not consistent with the sample; run the algorithm with $K = |\\Phi_1 \\wedge \\Phi_2|$, the chosen depth $D$, and the chosen $\\delta$. If the output is not $\\Phi_1 \\wedge \\Phi_2$ or is a larger formula, the completeness-and-minimality claim is false for the implemented algorithm.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Supplies LTL simplification and satisfiability checking behind the temporal and Boolean simplification heuristics that make GBE complete while pruning."},{"cited_title":"Sample efficient model-free reinforcement learning from LTL specifications with optimality guarantees","cited_arxiv_id":null,"evidence_quote":"Supplies the reinforcement-learning algorithms used to generate the strategy DTMCs in the first case study."}],"review_version":1}