pith. sign in

arxiv: 1907.03564 · v1 · pith:DOU5RL42new · submitted 2019-07-08 · 💻 cs.LO · cs.SY· eess.SY

Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions

Muhammad Syifa'ul Mufid , Dieky Adzkiya , Alessandro Abate This is my paper

Pith reviewed 2026-05-25 00:58 UTC · model grok-4.3

classification 💻 cs.LO cs.SYeess.SY
keywords max-plus linear systemspredicate abstractionbounded model checkingtime-difference specificationscompleteness thresholdtransientcyclicity
0
0 comments X

The pith

Predicate abstractions let bounded model checking verify time-difference properties in max-plus linear systems with an explicit completeness bound.

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

The paper develops predicate abstractions for max-plus linear systems by automatically selecting predicates from the system matrix and from the specifications. These abstractions support a bounded model checking procedure aimed at time-difference specifications, which capture relations between successive events. Experiments show the new abstractions perform better than prior MPL abstraction methods. The work also derives an explicit upper bound on the completeness threshold for the BMC search, expressed in terms of the transient length and cyclicity of the underlying system. If the abstractions are sound, this approach turns verification of timed discrete-event properties into a finite search problem.

Core claim

Predicate abstractions are constructed automatically from the system matrix and specifications for max-plus linear systems. A bounded model checking algorithm is then run on the abstract system to verify time-difference specifications. The abstractions improve experimentally over previous methods, and the completeness threshold for the BMC is bounded explicitly using the transient and cyclicity of the MPL system.

What carries the argument

The predicate abstraction, which selects predicates from the matrix and specs to produce a finite over-approximation on which BMC can be performed for time-difference properties.

If this is right

  • Time-difference specifications can be checked via BMC on the predicate-abstracted MPL system.
  • The predicate abstractions outperform existing MPL abstraction algorithms in experiments.
  • The BMC search depth is bounded above by a quantity computed from the transient and cyclicity of the MPL system.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same predicate-selection idea might be tried on other classes of linear systems over different semirings.
  • The explicit completeness bound could be used to decide when to fall back to unbounded techniques if no counterexample appears within the limit.
  • The method may scale to larger scheduling or logistics models once the abstraction is combined with existing BMC solvers.

Load-bearing premise

The predicates selected from the system matrix and specifications suffice to make the abstraction sound, so that satisfaction of a time-difference property in the abstract system implies satisfaction in the concrete MPL system.

What would settle it

A concrete MPL system and time-difference specification for which the BMC procedure on the predicate abstraction reports that the property holds, yet direct simulation or exact reachability analysis on the original system finds a violating trace.

Figures

Figures reproduced from arXiv: 1907.03564 by Alessandro Abate, Dieky Adzkiya, Muhammad Syifa'ul Mufid.

Figure 1
Figure 1. Figure 1: The abstract transition system via predicate abstractions [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: The refinement of the abstract transition in Figure 1. [PITH_FULL_IMAGE:figures/full_fig_p015_2.png] view at source ↗
read the original abstract

This paper introduces the abstraction of max-plus linear (MPL) systems via predicates. Predicates are automatically selected from system matrix, as well as from the specifications under consideration. We focus on verifying time-difference specifications, which encompass the relation between successive events in MPL systems. We implement a bounded model checking (BMC) procedure over a predicate abstraction of the given MPL system, to verify the satisfaction of time-difference specifications. Our predicate abstractions are experimentally shown to improve on existing MPL abstractions algorithms. Furthermore, with focus on the BMC algorithm, we can provide an explicit upper bound on the completeness threshold by means of the transient and the cyclicity of the underlying MPL system.

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

0 major / 2 minor

Summary. The paper introduces predicate abstractions for max-plus linear (MPL) systems, with predicates automatically selected from the system matrix and from time-difference specifications. It implements bounded model checking (BMC) over the resulting abstract system and claims both experimental improvement over prior MPL abstraction algorithms and an explicit upper bound on the BMC completeness threshold derived from the transient and cyclicity of the underlying MPL system.

Significance. If the soundness argument for the predicate abstraction holds and the experimental gains are reproducible, the work would strengthen automated verification for MPL systems by combining automatic predicate selection with a concrete completeness bound; the latter is a clear strength when the derivation is parameter-free and grounded in standard MPL properties.

minor comments (2)
  1. The abstract states that predicates are 'automatically selected' and that the abstraction 'improves' on prior methods, but the manuscript should clarify the precise selection heuristic and the quantitative metrics (e.g., state-space reduction, verification time) used in the experiments.
  2. The claim of an 'explicit upper bound' on the completeness threshold is attractive; the paper should state the bound explicitly (e.g., in terms of transient length and cyclicity index) and indicate whether it is tight or conservative.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their careful summary of the manuscript. The report lists no explicit major comments, so we provide no point-by-point rebuttals below. We remain available to address any specific technical questions the referee may have regarding soundness, the completeness threshold derivation, or the experimental comparison.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper's central claims rest on predicate abstraction for MPL systems with predicates drawn directly from the system matrix and specifications, followed by standard BMC. The explicit upper bound on the completeness threshold is derived from the transient and cyclicity properties of the underlying MPL system, which are established external facts about MPL dynamics rather than fitted or self-defined quantities. No equations reduce a prediction to a fitted input by construction, no load-bearing self-citation chains appear, and the soundness argument for the abstraction is stated as an assumption without circular reduction. The derivation is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

With only the abstract available, no specific free parameters or invented entities are identifiable. The work relies on standard concepts in max-plus algebra and model checking.

axioms (1)
  • standard math The max-plus semiring operations satisfy the necessary algebraic properties for linear systems.
    Fundamental to defining MPL systems in the paper.

pith-pipeline@v0.9.0 · 5650 in / 1278 out tokens · 31164 ms · 2026-05-25T00:58:22.483494+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages

  1. [1]

    IEEE Transactions on Automatic Control 58(12), 3039–3053 (2013)

    Adzkiya, D., De Schutter, B., Abate, A.: Finite abstracti ons of max-plus-linear systems. IEEE Transactions on Automatic Control 58(12), 3039–3053 (2013). https://doi.org/10.1109/TAC.2013.2273299

    work page doi:10.1109/tac.2013.2273299 2013

  2. [2]

    Discrete Event Dy namic Systems 26(1), 109–145 (2016)

    Adzkiya, D., Zhang, Y., Abate, A.: VeriSiMPL 2: An open-so urce software for the verification of max-plus-linear systems. Discrete Event Dy namic Systems 26(1), 109–145 (2016). https://doi.org/10.1007/s10626-015-02 18-x

    work page doi:10.1007/s10626-015-02 2016

  3. [3]

    In: Proc

    Alur, R., Dang, T., Ivanˇ ci´ c, F.: Progress on reachabili ty analysis of hy- brid systems using predicate abstraction. In: Proc. Intern ational Workshop on Hybrid Systems: Computation and Control. pp. 4–19. Sprin ger (2003). https://doi.org/10.1007/3-540-36580-X 4

    work page doi:10.1007/3-540-36580-x 2003

  4. [4]

    John Wiley & Sons Ltd ( 1992)

    Baccelli, F., Cohen, G., Olsder, G.J., Quadrat, J.P.: Syn chronization and Linearity: An Algebra for Discrete Event Systems. John Wiley & Sons Ltd ( 1992)

    work page 1992

  5. [5]

    MI T Press (2008)

    Baier, C., Katoen, J.P.: Principles of model checking. MI T Press (2008)

    work page 2008

  6. [6]

    In: In Proc

    Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Au tomatic predi- cate abstraction of C programs. In: In Proc. Programming Lan guage De- sign and Implementation 2001 (PLDI’01). vol. 36, pp. 203–21 3. ACM (2001). https://doi.org/10.1145/381694.378846

    work page doi:10.1145/381694.378846 2001

  7. [7]

    In: International Conference on Tools and Alg orithms for the Construction and Analysis of Systems

    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic mode l checking without BDDs. In: International Conference on Tools and Alg orithms for the Construction and Analysis of Systems. pp. 193–207. Spri nger (1999). https://doi.org/10.1007/3-540-49059-0 14

    work page doi:10.1007/3-540-49059-0 1999

  8. [8]

    Advances in Computers 58(11), 117–148 (2003)

    Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y., et al.: Bounded model checking. Advances in Computers 58(11), 117–148 (2003)

    work page 2003

  9. [9]

    Logical Methods in Computer S cience 2(5), 1–64 (2006)

    Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schup pan, V.: Linear encodings of bounded LTL model checking. Logical Methods in Computer S cience 2(5), 1–64 (2006). https://doi.org/10.2168/LMCS-2(5:5)2006

    work page doi:10.2168/lmcs-2(5:5)2006 2006

  10. [10]

    Journal of Th eoretical Biology 303, 128–140 (2012)

    Brackley, C.A., Broomhead, D.S., Romano, M.C., Thiel, M .: A Max-plus model of ribosome dynamics during mRNA translation. Journal of Th eoretical Biology 303, 128–140 (2012). https://doi.org/10.1016/j.jtbi.2012. 03.007

    work page doi:10.1016/j.jtbi.2012 2012

  11. [11]

    In: Proc

    Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An opensource tool f or symbolic model checking. In: Proc. of International Conference on Compute r Aided Verification (CA V’02). pp. 359–364. Springer (2002). https://doi.org/10.1007/3-540-45657-0 29

    work page doi:10.1007/3-540-45657-0 2002

  12. [12]

    In: Proc

    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Coun terexample- guided abstraction refinement. In: Proc. International Con ference on Com- puter Aided Verification 2000 (CA V’00). pp. 154–169. Spring er (2000). https://doi.org/10.1007/10722167 15

    work page doi:10.1007/10722167 2000

  13. [13]

    In: Proc

    Clarke, E., Grumberg, O., Talupur, M., Wang, D.: Making p redi- cate abstraction efficient. In: Proc. International Confere nce on Com- puter Aided Verification 2003 (CA V’03). pp. 126–140. Spring er (2003). https://doi.org/10.1007/978-3-540-45069-6 14

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

  14. [14]

    In: International Works hop on Verifica- tion, Model Checking, and Abstract Interpretation

    Clarke, E., Kroening, D., Ouaknine, J., Strichman, O.: C ompleteness and com- plexity of bounded model checking. In: International Works hop on Verifica- tion, Model Checking, and Abstract Interpretation. pp. 85– 96. Springer (2004). https://doi.org/10.1007/978-3-540-24622-0 9

    work page doi:10.1007/978-3-540-24622-0 2004

  15. [15]

    Formal Methods in System Design 25(2-3), 105–127 (2004)

    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Pred icate abstraction of ANSI- C programs using SAT. Formal Methods in System Design 25(2-3), 105–127 (2004). https://doi.org/10.1023/B:FORM.0000040025.89719.f3 BMC of MPL Systems via PA 19

    work page doi:10.1023/b:form.0000040025.89719.f3 2004

  16. [16]

    In: International Con ference on The- ory and Applications of Satisfiability Testing

    Clarke, E., Talupur, M., Veith, H., Wang, D.: SAT based pr edicate ab- straction for hardware verification. In: International Con ference on The- ory and Applications of Satisfiability Testing. pp. 78–92. S pringer (2003). https://doi.org/10.1007/978-3-540-24605-3 7

    work page doi:10.1007/978-3-540-24605-3 2003

  17. [17]

    ACM Transactions on Programming Languages and Systems (TOPLAS ) 16(5), 1512– 1542 (1994)

    Clarke, E.M., Grumberg, O., Long, D.E.: Model checking a nd abstraction. ACM Transactions on Programming Languages and Systems (TOPLAS ) 16(5), 1512– 1542 (1994). https://doi.org/10.1145/186025.186051

    work page doi:10.1145/186025.186051 1994

  18. [18]

    Theoretical computer science 293(1), 189–217 (2003)

    Comet, J.P.: Application of max-plus algebra to biologi cal sequence comparisons. Theoretical computer science 293(1), 189–217 (2003). https://doi.org/10.1016/S0304-3975(02)00237-2

    work page doi:10.1016/s0304-3975(02)00237-2 2003

  19. [19]

    In: Proc

    Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Proc. In- ternational Conference on Computer Aided Verification (CA V ’99). pp. 160–171. Springer (1999). https://doi.org/10.1007/3-540-48683- 6 16

    work page doi:10.1007/3-540-48683- 1999

  20. [20]

    Linear Algebra and its Ap plications 307(1-3), 103–117 (2000)

    De Schutter, B.: On the ultimate behavior of the sequence of consecutive powers of a matrix in the max-plus algebra. Linear Algebra and its Ap plications 307(1-3), 103–117 (2000). https://doi.org/10.1016/S0024-3795(00 )00013-6

    work page doi:10.1016/s0024-3795(00 2000

  21. [21]

    In: Proc

    Flanagan, C., Qadeer, S.: Predicate abstraction for sof tware verification. In: Proc. 29th Principles of Programming Languages (POPL’02). vol. 3 7, pp. 191–202. ACM (2002). https://doi.org/10.1145/503272.503291

    work page doi:10.1145/503272.503291 2002

  22. [22]

    In: Proc

    Graf, S., Sa ¨ ıdi, H.: Construction of abstract state gra phs with PVS. In: Proc. International Conference on Computer Aided Verification (C A V’97). pp. 72–83. Springer (1997). https://doi.org/10.1007/3-540-63166- 6 10

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

  23. [23]

    Automatica 37(7), 1085–1091 (July 2001)

    Heemels, W., De Schutter, B., Bemporad, A.: Equivalence of hy- brid dynamical models. Automatica 37(7), 1085–1091 (July 2001). https://doi.org/10.1016/S0005-1098(01)00059-0

    work page doi:10.1016/s0005-1098(01)00059-0 2001

  24. [24]

    Princeton University Press (2014)

    Heidergott, B., Olsder, G.J., Van der Woude, J.: Max Plus at Work: Modeling and Analysis of Synchronized Systems: A Course on Max-Plus A lgebra and its Applications. Princeton University Press (2014)

    work page 2014

  25. [25]

    Saturn: A SAT-Based Tool for Bug Detection

    Heljanko, K., Junttila, T., Latvala, T.: Incremental an d complete bounded model checking for full PLTL. In: Proc. of International Con ference on Computer Aided Verificationn (CA V’05). pp. 98–111. Sprin ger (2005). https://doi.org/10.1007/11513988 10

    work page doi:10.1007/11513988 2005

  26. [26]

    In: Proc

    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Laz y abstraction. In: Proc. of the ACM Symposium on Principles of Programming Languages (POPL’02). pp. 58–70 (2002). https://doi.org/10.1145/503272.503279

    work page doi:10.1145/503272.503279 2002

  27. [27]

    In: Proc

    Imaev, A., Judd, R.P.: Hierarchial modeling of manufact uring systems using max- plus algebra. In: Proc. American Control Conference, 2008. pp. 471–476 (June 2008)

    work page 2008

  28. [28]

    In: Proc

    Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simp le is better: Efficient bounded model checking for past LTL. In: Proc. of International Work shop on Verification, Model Checking, and Abstract Interpretation (VMCAI’05). p p. 380–395. Springer (2005). https://doi.org/10.1007/978-3-540-30579-8 25

    work page doi:10.1007/978-3-540-30579-8 2005

  29. [29]

    In: Proc

    Mufid, M.S., Adzkiya, D., Abate, A.: Tropical abstractio ns of max-plus lin- ear systems. In: Proc. of International Conference on Forma l Modeling and Analysis of Timed Systems (FORMATS’18). pp. 271–287. Sprin ger (2018). https://doi.org/10.1007/978-3-030-00151-3 16

    work page doi:10.1007/978-3-030-00151-3 2018