Pith. sign in

REVIEW 2 major objections 2 minor 52 references

Infinite State Model Checking by Learning Transitive Relations

T0 review · 2 major / 2 minor · reviewed 2026-05-23 · grok-4.3

Challenge this review Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Extending infinite-state systems with transitive relations until their diameter is finite allows safety to be proved by checking that no error is reachable in D steps.

desk verdict The paper combines recurrence analysis with projections to discover disjunctive transitive relations that can make the diameter finite for safety proofs in infinite-state systems. read the letter →

arxiv 2502.04761 v4 submitted 2025-02-07 cs.LO

Florian Frohn , Jürgen Giesl This is my paper · ORCID
classification cs.LO
keywords infinite-statesystemssafetyverificationmodelcheckingtransitiverelationsrecurrenceanalysisdiameterprojectionsLoAT
checked against Foundation.ArithmeticFromLogicCost.FunctionalEquation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper sets out to prove safety of infinite-state systems by iteratively extending the transition relation with additional transitive relations. These relations are deduced via recurrence analysis, with projections added to capture disjunctive relations that standard recurrence methods miss. Once the diameter D becomes finite, meaning a fixed number of steps reaches all possible states from any start, safety reduces to a simple bounded reachability query that rules out error states in D steps. The method is realized in the LoAT tool and shown to match or exceed existing approaches on benchmarks.

What carries the argument

The diameter D of the extended transition relation, obtained by adding transitive relations from recurrence analysis and projections, which guarantees that D steps suffice to reach every reachable state from any initial state.

What would settle it

An infinite-state system that remains safe yet admits no finite collection of transitive relations that render its diameter finite, or a case where the analysis fails to locate such relations even though they exist.

Watch

Extended reading notes

Core claim

By extending the analyzed system by transitive relations until its diameter D becomes finite, safety can be proved by checking that no error state is reachable in D steps.

Load-bearing premise

Recurrence analysis combined with projections can discover the transitive relations required to make the diameter finite for the infinite-state systems under consideration.

Editorial extensions

If this is right

  • Safety verification for infinite-state systems reduces to a finite bounded model-checking query whose bound is the computed diameter D.
  • Disjunctive transitive relations become discoverable even when basic recurrence analysis yields only conjunctive ones.
  • The same extension process applies uniformly to any system whose transition relation can be represented in the input language of the LoAT tool.
  • Once D is finite, any standard finite-state model checker can be used to discharge the final safety query.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The same recurrence-plus-projection technique might be reusable inside termination provers that already compute recurrence relations.
  • If the diameter stays infinite after a reasonable number of extensions, the method could be combined with abstraction or widening operators to still obtain useful partial results.
  • The finite-diameter property might serve as a sufficient condition for other properties beyond safety, such as bounded response.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

2 major / 2 minor

Summary. The paper proposes extending infinite-state transition systems with transitive relations discovered via recurrence analysis (augmented by projections to obtain disjunctive relations) until the diameter D becomes finite; safety is then reduced to a D-step bounded reachability check for error states. The method is implemented in LoAT and shown empirically competitive with existing tools on a benchmark suite.

Significance. If the central reduction is sound, the technique supplies a new route from infinite-state safety to finite bounded model checking by learning transitive closures that collapse path lengths. The combination of recurrence analysis with projections to handle disjunctions is a concrete technical contribution, and the empirical evaluation provides evidence of practical utility. However, the absence of a termination characterization or preservation proof for the diameter reduction limits the theoretical scope.

major comments (2)
  1. [Abstract / Approach Overview] The central claim (that recurrence analysis plus projections suffice to produce a finite diameter while preserving the reachable set) is load-bearing but lacks a supporting theorem or class characterization; the abstract states the approach but provides no formal argument that the added relations are both sound (exact reachable set) and complete enough to bound all paths by D.
  2. [Approach Description] No argument is given that the iterative extension process is guaranteed to terminate with finite D on the target class of systems, nor that the D-step check remains a decision procedure for safety once the relations are added; if the analysis misses a required relation the diameter stays infinite and the method is inapplicable.
minor comments (2)
  1. [Abstract] The abstract mentions 'constantly many steps' but does not define the precise notion of diameter used (e.g., whether it is the standard graph diameter of the state space or a syntactic diameter over the extended transition relation).
  2. [Empirical Evaluation] Implementation details on how projections are combined with recurrence analysis inside LoAT would benefit from a short pseudocode or example in the evaluation section to aid reproducibility.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback. Our responses to the major comments are provided below. The manuscript presents a practical technique whose value is demonstrated empirically; we do not claim a general decision procedure or termination guarantee.

read point-by-point responses

  1. Referee: [Abstract / Approach Overview] The central claim (that recurrence analysis plus projections suffice to produce a finite diameter while preserving the reachable set) is load-bearing but lacks a supporting theorem or class characterization; the abstract states the approach but provides no formal argument that the added relations are both sound (exact reachable set) and complete enough to bound all paths by D.

    Authors: The added relations are derived from recurrence analysis and are therefore valid (they correspond to actual paths in the original system), so reachability is preserved while diameters are reduced. The reduction to a D-step check is sound whenever a finite D is obtained. We do not supply a class characterization or completeness theorem because the method is not intended to be complete; it is a heuristic that succeeds on many systems in the benchmark. A short clarifying paragraph on soundness can be added to the approach overview. revision: partial

  2. Referee: [Approach Description] No argument is given that the iterative extension process is guaranteed to terminate with finite D on the target class of systems, nor that the D-step check remains a decision procedure for safety once the relations are added; if the analysis misses a required relation the diameter stays infinite and the method is inapplicable.

    Authors: The iterative process is not guaranteed to terminate; it is a heuristic whose success depends on the system. When a finite D is reached the D-step check is sufficient to prove safety, as every reachable state is reachable in at most D steps in the extended system. The method simply does not apply when the diameter remains infinite, which is consistent with the competitive (rather than uniformly superior) experimental results. A general termination argument is not provided, as the underlying problem is undecidable in general. revision: no

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: derivation relies on independent recurrence analysis

full rationale

The approach extends the system with transitive relations found by recurrence analysis (plus projections for disjunctive cases) until diameter D is finite, then checks reachability in D steps. This does not reduce by construction to its inputs: the relations are not defined in terms of D, no parameters are fitted to the safety outcome, and no self-citation chain is invoked to force uniqueness or the central claim. The method applies established recurrence techniques in a new combination without self-definitional loops or renaming of known results. The derivation chain is therefore self-contained against external benchmarks.

Assumptions & free parameters 0 free parameters · 2 assumptions · 0 invented entities

The paper builds on standard concepts from model checking and recurrence relations without introducing new free parameters or invented entities; the central claim rests on domain assumptions about the utility of transitive relations and recurrence analysis.

assumptions (2)
  • domain assumption Transitive relations can be added to transition systems to bound the diameter of the reachable state space
    This is the core mechanism invoked to reduce infinite-state reachability to finite checks.
  • domain assumption Recurrence analysis identifies relations in the transition relation of the system
    Used as the basis for deducing the transitive relations.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Infinite State Model Checking by Learning Transitive Relations." pith.science (2026). https://pith.science/paper/2502.04761

@misc{pith2026250204761,
  author       = {Pith},
  title        = {Pith review of: Infinite State Model Checking by Learning Transitive Relations},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/2502.04761}},
  note         = {Machine review of arXiv:2502.04761}
}
read the original abstract

We propose a new approach for proving safety of infinite state systems. It extends the analyzed system by transitive relations until its diameter D becomes finite, i.e., until constantly many steps suffice to cover all reachable states, irrespective of the initial state. Then we can prove safety by checking that no error state is reachable in D steps. To deduce transitive relations, we use recurrence analysis. While recurrence analyses can usually find conjunctive relations only, our approach also discovers disjunctive relations by combining recurrence analysis with projections. An empirical evaluation of the implementation of our approach in our tool LoAT shows that it is highly competitive with the state of the art.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

52 extracted references · 52 canonical work pages

  1. [1]

    Data-driven invariant learning for probabilistic programs

    Alt, L., Blicha, M., Hyv¨ arinen, A.E.J., Sharygina, N.: SolCMC: Solidity compiler’s model checker. In: CA V ’22. pp. 325–338. LNCS 133 71 (2022). https://doi.org/10.1007/978-3-031-13185-1 16

    work page doi:10.1007/978-3-031-13185-1 2022

  2. [2]

    In: ATV A ’05

    Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: ATV A ’05. pp. 474–488. LNCS 370 7 (2005). https://doi.org/10.1007/11562948 35

    work page doi:10.1007/11562948 2005

  3. [3]

    www.SMT-LIB.org (2016)

    Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiabilit y Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)

    work page 2016

  4. [4]

    Advances in Computers 58, 117–148 (2003)

    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y.: Bounded model checking. Advances in Computers 58, 117–148 (2003). https://doi.org/10.1016/S0065-2458(03)58003-2

    work page doi:10.1016/s0065-2458(03)58003-2 2003

  5. [5]

    Cosler, C

    Blicha, M., Britikov, K., Sharygina, N.: The Golem Horn solver. In: CA V ’23. pp. 209–223. LNCS 13965 (2023). https://doi.org/10.1007/978-3-031-37703-7 10

    work page doi:10.1007/978-3-031-37703-7 2023

  6. [7]

    In: VMCAI ’11

    Bradley, A.R.: SAT-based model checking without unrolli ng. In: VMCAI ’11. pp. 70–87. LNCS 6538 (2011). https://doi.org/10.1007/978-3-642-18275-4 7

    work page doi:10.1007/978-3-642-18275-4 2011

  7. [8]

    Bremner, D.: Incremental convex hull algorithms are not o utput sensitive. Discret. Comput. Geom. 21(1), 57–68 (1999). https://doi.org/10.1007/PL00009410

    work page doi:10.1007/pl00009410 1999

  8. [10]

    In: EuroS&P ’16

    Calzavara, S., Grishchenko, I., Maffei, M.: HornDroid: Practical and sound static analysis of Android applications by SMT solving. In: EuroS&P ’16. pp. 47–62. IEE E (2016). https://doi.org/10.1109/EuroSP.2016.16

    work page doi:10.1109/eurosp.2016.16 2016

Show all 52 references
  1. [11]

    CHC Competition, https://chc-comp.github.io

  2. [12]

    In: CA V ’00

    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Co unterexample- guided abstraction refinement. In: CA V ’00. pp. 154–169. LNC S 1855 (2000). https://doi.org/10.1007/10722167 15

    2000 doi

  3. [13]

    Machine In- telligence 7, 91–99 (1972)

    Cooper, D.C.: Theorem proving in arithmetic without mul tiplication. Machine In- telligence 7, 91–99 (1972)

    1972

  4. [14]

    De Angelis, E., Govind V K, H.: CHC-COMP 2023: Competitio n report (2023), https://chc-comp.github.io/2023/CHC COMP 2023 Competition Report.pdf

    2023

  5. [15]

    In: CA V ’14

    Dutertre, B.: Yices 2.2. In: CA V ’14. pp. 737–744. LNCS 8559 (2014). https://doi.org/10.1007/978-3-319-08867-9 49

    2014 doi

  6. [16]

    A cademic Press (1972)

    Enderton, H.B.: A Mathematical Introduction to Logic. A cademic Press (1972)

    1972

  7. [18]

    Ernst, G., Morales, J.F.: CHC-COMP 2024: Competition re port (2024), https://chc-comp.github.io/2024/CHC-COMP%202024%20Report%20-%20HCSV.pdf

    2024

  8. [19]

    In: FMCAD ’15

    Farzan, A., Kincaid, Z.: Compositional recurrence anal ysis. In: FMCAD ’15. pp. 57–64 (2015). https://doi.org/10.1109/FMCAD.2015.7542253

    2015 doi

  9. [20]

    In: TACAS ’20

    Frohn, F.: A calculus for modular loop acceleration. In: TACAS ’20. pp. 58–76. LNCS 12078 (2020). https://doi.org/10.1007/978-3-030-45190-5 4

    2020 doi

  10. [21]

    In: IJCAR ’22

    Frohn, F., Giesl, J.: Proving non-termination and lower runtime bounds with LoAT (system description). In: IJCAR ’22. pp. 712–722. LNCS 1338 5 (2022). https://doi.org/10.1007/978-3-031-10769-6 41

    2022 doi

  11. [22]

    In: CADE ’23

    Frohn, F., Giesl, J.: Proving non-termination by Accele ration Driven Clause Learning. In: CADE ’23. pp. 220–233. LNCS 14132 (2023 ). https://doi.org/10.1007/978-3-031-38499-8 13

    2023 doi

  12. [23]

    In: SAS ’23

    Frohn, F., Giesl, J.: ADCL: Acceleration Driven Clause L earning for con- strained Horn clauses. In: SAS ’23. pp. 259–285. LNCS 14284 ( 2023). https://doi.org/10.1007/978-3-031-44245-2 13

    2023 doi

  13. [25]

    CoRR abs/2502.04761 (2025)

    Frohn, F., Giesl, J.: Infinite state model checking by lea rning transitive relations. CoRR abs/2502.04761 (2025). https://doi.org/10.48550/arXiv.2502.04761

    2025 doi arXiv

  14. [26]

    Infinite State Model Checking by Learning Transitive Relations

    Frohn, F., Giesl, J.: Evaluation of “Infinite State Model Checking by Learning Transitive Relations” (2025), https://loat-developers.github.io/trl-eval/

    2025

  15. [27]

    Frohn, F., Giesl, J.: LoAT website, https://loat-developers.github.io/LoAT/

  16. [28]

    Genov, B.: The Convex Hull Problem in Practice: Improvin g the Running Time of the Double Description Method. Ph.D. thesis, Bremen Univer sity, Germany (2015), https://media.suub.uni-bremen.de/handle/elib/833

    2015

  17. [29]

    In: TACAS ’19

    Giesl, J., Rubio, A., Sternagel, C., Waldmann, J., Yamad a, A.: The termination and complexity competition. In: TACAS ’19. pp. 156–166. LNC S 11429 (2019). https://doi.org/10.1007/978-3-030-17502-3 10

    2019 doi

  18. [30]

    In: CA V ’97

    Graf, S., Sa ¨ ıdi, H.: Construction of abstract state gra phs with PVS. In: CA V ’97. pp. 72–83. LNCS 1254 (1997). https://doi.org/10.1007/3-540-63166-6 10

    1997 doi

  19. [31]

    In: CA V ’15

    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: CA V ’15. pp. 343–361. LNCS 9206 ( 2015). https://doi.org/10.1007/978-3-319-21690-4 20

    2015 doi

  20. [32]

    In: Cousot, R., Martel, M

    Heizmann, M., Jones, N.D., Podelski, A.: Size-change te rmination and transition invariants. In: Cousot, R., Martel, M. (eds.) SAS ’10. pp. 22 –50. LNCS 6337 (2010). https://doi.org/10.1007/978-3-642-15769-1 4

    2010 doi

  21. [33]

    In: FMCAD ’18

    Hojjat, H., R¨ ummer, P.: The Eldarica Horn solver. In: FMCAD ’18. pp. 1–7 (2018). https://doi.org/10.23919/FMCAD.2018.8603013

    2018 doi

  22. [34]

    In: FMCAD ’16

    Jovanovic, D., Dutertre, B.: Property-directed k-indu ction. In: FMCAD ’16. pp. 85–92 (2016). https://doi.org/10.1109/FMCAD.2016.7886665

    2016 doi

  23. [35]

    In: CA V ’16

    Kahsai, T., R¨ ummer, P., Sanchez, H., Sch¨ af, M.: JayHorn: A framework for verifying Java programs. In: CA V ’16. pp. 352–358. LNCS 9779 (2016). https://doi.org/10.1007/978-3-319-41528-4 19

    2016 doi

  24. [36]

    In: PLDI ’17

    Kincaid, Z., Breck, J., Boroujeni, A.F., Reps, T.W.: Com positional recurrence analysis revisited. In: PLDI ’17. pp. 248–262 (2 017). https://doi.org/10.1145/3062341.3062373

    doi

  25. [37]

    Formal Methods Syst

    Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based mod el checking for recursive programs. Formal Methods Syst. Des. 48(3), 175–205 (2016). https://doi.org/10.1007/s10703-016-0249-4 26 F. Frohn, J. Giesl

    2016 doi

  26. [38]

    In: TACAS ’16

    Koneˇ cn´ y, F.: PTIME computation of transitive closure s of octag- onal relations. In: TACAS ’16. pp. 645–661. LNCS 9636 (2016) . https://doi.org/10.1007/978-3-662-49674-9 42

    2016 doi

  27. [39]

    In: CA V ’20

    Krishnan, H.G.V., Chen, Y., Shoham, S., Gurfinkel, A.: Gl obal guidance for local generalization in model checking. In: CA V ’20. pp. 101–125. LNCS 12225 (2020). https://doi.org/10.1007/978-3-030-53291-8 7

    2020 doi

  28. [40]

    , Wintersteiger, C.M.: Loop summarization using state and transition invariants

    Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A. , Wintersteiger, C.M.: Loop summarization using state and transition invariants. Form al Methods Syst. Des. 42(3), 221–261 (2013). https://doi.org/10.1007/S10703-012-0176-Y

    2013 doi

  29. [41]

    In: CA V ’10

    Kroening, D., Sharygina, N., Tsitovich, A., Winterstei ger, C.M.: Termination anal- ysis with compositional transition invariants. In: CA V ’10 . pp. 89–103. LNCS 6174 (2010). https://doi.org/10.1007/978-3-642-14295-6 9

    2010 doi

  30. [42]

    In: FM ’15

    Kroening, D., Lewis, M., Weissenbacher, G.: Proving saf ety with trace automata and bounded model checking. In: FM ’15. pp. 325–341. LNCS 910 9 (2015). https://doi.org/10.1007/978-3-319-19249-9 21

    2015 doi

  31. [43]

    ACM Trans

    Matsushita, Y., Tsukada, T., Kobayashi, N.: RustHorn: CHC-based verification for Rust programs. ACM Trans. Program. Lang. Syst. 43(4), 15:1–15:54 (2021). https://doi.org/10.1145/3462205

    2021 doi

  32. [44]

    In: CA V ’03

    McMillan, K.L.: Interpolation and SAT-based model chec king. In: CA V ’03. pp. 1–13. LNCS 2725 (2003). https://doi.org/10.1007/978-3-540-45069-6 1

    2003 doi

  33. [45]

    In : CA V ’06

    McMillan, K.L.: Lazy abstraction with interpolants. In : CA V ’06. pp. 123–136. LNCS 4144 (2006). https://doi.org/10.1007/11817963 14

    2006 doi

  34. [46]

    In: TACAS ’08

    de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: TACAS ’08. pp. 337–340. LNCS 4963 (2008). https://doi.org/10.1007/978-3-540-78800-3 24

    2008 doi

  35. [47]

    In: RP ’24

    Pimpalkhare, N., Kincaid, Z.: Semi-linear V ASR for over -approximate semi-linear transition system reachability. In: RP ’24. pp. 154–166. LN CS 15050 (2024). https://doi.org/10.1007/978-3-031-72621-7 11

    2024 doi

  36. [48]

    In: LICS ’04

    Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS ’04. pp. 32–41 (2004). https://doi.org/10.1109/LICS.2004.1319598

    2004 doi

  37. [49]

    In: TACAS ’11

    Podelski, A., Rybalchenko, A.: Transition invariants a nd transition predicate ab- straction for program termination. In: TACAS ’11. pp. 3–10. LCNS 6605 (2011). https://doi.org/10.1007/978-3-642-19835-9 2

    2011 doi

  38. [50]

    In: FM ’24

    Promies, V., ´Abrah´ am, E.: A divide-and-conquer approach to variable el imina- tion in linear real arithmetic. In: FM ’24. pp. 131–148. LNCS 14933 (2024). https://doi.org/10.1007/978-3-031-71162-6 7

    2024 doi

  39. [51]

    In: FMCAD ’00

    Sheeran, M., Singh, S., St ˚ almarck, G.: Checking safety properties using in- duction and a SAT-solver. In: FMCAD ’00. pp. 108–125. LNCS 19 54 (2000). https://doi.org/10.1007/3-540-40922-X 8

    2000 doi

  40. [52]

    In: CA V ’19

    Silverman, J., Kincaid, Z.: Loop summarization with rat ional vec- tor addition systems. In: CA V ’19. pp. 97–115. LNCS 11562 (20 19). https://doi.org/10.1007/978-3-030-25543-5 7

    doi

  41. [53]

    In: TACAS ’24

    Solanki, M., Chatterjee, P., Lal, A., Roy, S.: Accelerat ed bounded model checking using interpolation based summaries. In: TACAS ’24. pp. 155 –174. LNCS 14571 (2024). https://doi.org/10.1007/978-3-031-57249-4 8

    2024 doi

  42. [54]

    In: TACAS ’11

    Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kro ening, D.: Loop summariza- tion and termination analysis. In: TACAS ’11. pp. 81–95. LNC S 6605 (2011)

    2011

  43. [55]

    In: VMCAI ’22

    Wesley, S., Christakis, M., Navas, J.A., Trefler, R.J., W ¨ ustholz, V., Gurfinkel, A.: Verifying Solidity smart contracts via communication abstrac- tion in SmartACE. In: VMCAI ’22. pp. 425–449. LNCS 13182 (2022). https://doi.org/10.1007/978-3-030-94583-1 21 Infinite State Model...

    2022 doi

  44. [56]

    In: SAS ’18

    Zuleger, F.: Inductive termination proofs with transit ion invariants and their re- lationship to the size-change abstraction. In: SAS ’18. pp. 423–444. LNCS 11002 (2018). https://doi.org/10.1007/978-3-319-99725-4 25 28 F. Frohn, J. Giesl A Appendix A.1 Proof of Thm. 22 Theore...

    2018 doi

Pith tools

Reviewed May 23, 2026 · model on record in the stance chip above.