pith. sign in

arxiv: 2502.04761 · v4 · submitted 2025-02-07 · 💻 cs.LO

Infinite State Model Checking by Learning Transitive Relations

Florian Frohn , J\"urgen Giesl This is my paper

Pith reviewed 2026-05-23 04:29 UTC · model grok-4.3

classification 💻 cs.LO
keywords infinite-state systemssafety verificationmodel checkingtransitive relationsrecurrence analysisdiameterprojectionsLoAT
0
0 comments X

The pith

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.

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

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.

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.

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.

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.

Where Pith is reading between the lines

These are 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.

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.

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.

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

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

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.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 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.

axioms (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.

pith-pipeline@v0.9.0 · 5627 in / 1355 out tokens · 36427 ms · 2026-05-23T04:29:19.463392+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

52 extracted references · 52 canonical work pages · 1 internal anchor

  1. [1]

    In: CA V ’22

    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]

    In: CA V ’23

    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

  9. [11]

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

    work page

  10. [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

    work page doi:10.1007/10722167 2000

  11. [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)

    work page 1972

  12. [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

    work page 2023

  13. [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

    work page doi:10.1007/978-3-319-08867-9 2014

  14. [16]

    A cademic Press (1972)

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

    work page 1972

  15. [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

    work page 2024

  16. [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

    work page doi:10.1109/fmcad.2015.7542253 2015

  17. [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

    work page doi:10.1007/978-3-030-45190-5 2020

  18. [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

    work page doi:10.1007/978-3-031-10769-6 2022

  19. [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

    work page doi:10.1007/978-3-031-38499-8 2023

  20. [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

    work page doi:10.1007/978-3-031-44245-2 2023

  21. [25]

    Infinite State Model Checking by Learning Transitive Relations

    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

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.2502.04761 2025

  22. [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/

    work page 2025

  23. [27]

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

    work page

  24. [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

    work page 2015

  25. [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

    work page doi:10.1007/978-3-030-17502-3 2019

  26. [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

    work page doi:10.1007/3-540-63166-6 1997

  27. [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

    work page doi:10.1007/978-3-319-21690-4 2015

  28. [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

    work page doi:10.1007/978-3-642-15769-1 2010

  29. [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

    work page doi:10.23919/fmcad.2018.8603013 2018

  30. [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

    work page doi:10.1109/fmcad.2016.7886665 2016

  31. [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

    work page doi:10.1007/978-3-319-41528-4 2016

  32. [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

    work page doi:10.1145/3062341.3062373

  33. [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

    work page doi:10.1007/s10703-016-0249-4 2016

  34. [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

    work page doi:10.1007/978-3-662-49674-9 2016

  35. [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

    work page doi:10.1007/978-3-030-53291-8 2020

  36. [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

    work page doi:10.1007/s10703-012-0176-y 2013

  37. [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

    work page doi:10.1007/978-3-642-14295-6 2010

  38. [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

    work page doi:10.1007/978-3-319-19249-9 2015

  39. [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

    work page doi:10.1145/3462205 2021

  40. [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

    work page doi:10.1007/978-3-540-45069-6 2003

  41. [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

    work page doi:10.1007/11817963 2006

  42. [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

    work page doi:10.1007/978-3-540-78800-3 2008

  43. [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

    work page doi:10.1007/978-3-031-72621-7 2024

  44. [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

    work page doi:10.1109/lics.2004.1319598 2004

  45. [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

    work page doi:10.1007/978-3-642-19835-9 2011

  46. [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

    work page doi:10.1007/978-3-031-71162-6 2024

  47. [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

    work page doi:10.1007/3-540-40922-x 2000

  48. [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

    work page doi:10.1007/978-3-030-25543-5

  49. [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

    work page doi:10.1007/978-3-031-57249-4 2024

  50. [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)

    work page 2011

  51. [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 Checking by Learning Transitive Relati ons 27

    work page doi:10.1007/978-3-030-94583-1 2022

  52. [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 Theorem 22. If TRL (T ) returns safe, then T is safe. Proof. Consider the SMT problem ...

    work page doi:10.1007/978-3-319-99725-4 2018