Skip to main content
SpringerLink
Log in
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11750))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    For the sake of simplicity, we write the elements of \(\texttt {fin}_i\) in a strictly increasing order.

  2. 2.

    In this paper, we always use \(p\equiv x_i-x_j\ge c\) as a predicate.

  3. 3.

    Notice that, in Definition 6 we consider \(\mathcal {AP}\) as a set of time-difference propositions.

  4. 4.

    Notice a loop-back transition from \(\hat{s}_k\) to \(\hat{s}_l\) in \(\pi _{loop}\).

References

  1. Adzkiya, D., De Schutter, B., Abate, A.: Finite abstractions of max-plus-linear systems. IEEE Trans. Autom. Control. 58(12), 3039–3053 (2013). https://doi.org/10.1109/TAC.2013.2273299

    Article  MathSciNet  MATH  Google Scholar 

  2. Adzkiya, D., Zhang, Y., Abate, A.: \(\text{VeriSiMPL}\) 2: an open-sourcesoftware for the verification of max-plus-linear systems. Discrete Event Dyn. Syst. 26(1), 109–145 (2016). https://doi.org/10.1007/s10626-015-0218-x

    Article  MathSciNet  MATH  Google Scholar 

  3. Alur, R., Dang, T., Ivančić, F.: Progress on reachability analysis of hybrid systems using predicate abstraction. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 4–19. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36580-X_4

    Chapter  MATH  Google Scholar 

  4. Baccelli, F., Cohen, G., Olsder, G.J., Quadrat, J.P.: Synchronization and Linearity: An Algebra for Discrete Event Systems. Wiley, Chichester (1992)

    MATH  Google Scholar 

  5. Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  6. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Proceedings of Programming Language Design and Implementation 2001 (PLDI 2001), vol. 36, pp. 203–213. ACM (2001). https://doi.org/10.1145/381694.378846

    Article  Google Scholar 

  7. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  9. Biere, A., Heljanko, K., Junttila, T., Latvala, T., Schuppan, V.: Linear encodings of bounded LTL model checking. Log. Methods Comput. Sci. 2(5), 1–64 (2006). https://doi.org/10.2168/LMCS-2(5:5)2006

    Article  MathSciNet  MATH  Google Scholar 

  10. Brackley, C.A., Broomhead, D.S., Romano, M.C., Thiel, M.: A Max-plus model of ribosome dynamics during mRNA translation. J. Theor. Biol. 303, 128–140 (2012). https://doi.org/10.1016/j.jtbi.2012.03.007

    Article  MathSciNet  MATH  Google Scholar 

  11. Cimatti, A., et al.: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_29

    Chapter  Google Scholar 

  12. Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_15

    Chapter  Google Scholar 

  13. Clarke, E., Grumberg, O., Talupur, M., Wang, D.: Making predicate abstraction efficient. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 126–140. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45069-6_14

    Chapter  Google Scholar 

  14. Clarke, E., Kroening, D., Ouaknine, J., Strichman, O.: Completeness and complexity of bounded model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 85–96. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24622-0_9

    Chapter  MATH  Google Scholar 

  15. Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI-C programs using SAT. Form. Methods Syst. Des. 25(2–3), 105–127 (2004). https://doi.org/10.1023/B:FORM.0000040025.89719.f3

    Article  MATH  Google Scholar 

  16. Clarke, E., Talupur, M., Veith, H., Wang, D.: SAT based predicate abstraction for hardware verification. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 78–92. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24605-3_7

    Chapter  Google Scholar 

  17. Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(5), 1512–1542 (1994). https://doi.org/10.1145/186025.186051

    Article  Google Scholar 

  18. Comet, J.P.: Application of max-plus algebra to biological sequence comparisons. Theor. Comput. Sci. 293(1), 189–217 (2003). https://doi.org/10.1016/S0304-3975(02)00237-2

    Article  MathSciNet  MATH  Google Scholar 

  19. Das, S., Dill, D.L., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48683-6_16

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  21. Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Proceedings of the 29th Principles of Programming Languages (POPL 2002), vol. 37, pp. 191–202. ACM (2002). https://doi.org/10.1145/503272.503291

  22. Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). https://doi.org/10.1007/3-540-63166-6_10

    Chapter  Google Scholar 

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

    Article  MATH  Google Scholar 

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

    Google Scholar 

  25. Heljanko, K., Junttila, T., Latvala, T.: Incremental and complete bounded model checking for full PLTL. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 98–111. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_10

    Chapter  Google Scholar 

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

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

    Google Scholar 

  28. Latvala, T., Biere, A., Heljanko, K., Junttila, T.: Simple is better: efficient bounded model checking for past LTL. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 380–395. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_25

    Chapter  MATH  Google Scholar 

  29. Mufid, M.S., Adzkiya, D., Abate, A.: Tropical abstractions of max-plus linear systems. In: Jansen, D.N., Prabhakar, P. (eds.) FORMATS 2018. LNCS, vol. 11022, pp. 271–287. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00151-3_16

    Chapter  MATH  Google Scholar 

  30. Mufid, M.S., Adzkiya, D., Abate, A.: Bounded model checking of max-plus linear systems via predicate abstractions. arXiv e-prints arXiv:1907.03564, July 2019

Download references

Acknowledgements

The first author is supported by Indonesia Endowment Fund for Education (LPDP), while the third acknowledges the support of the Alan Turing Institute, London, UK.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Oxford, Oxford, UK

    Muhammad Syifa’ul Mufid & Alessandro Abate

  2. Department of Mathematics, Institut Teknologi Sepuluh Nopember, Surabaya, Indonesia

    Dieky Adzkiya

Authors
  1. Muhammad Syifa’ul Mufid
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dieky Adzkiya
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alessandro Abate
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Muhammad Syifa’ul Mufid .

Editor information

Editors and Affiliations

  1. Université Paris 13, Villetaneuse, France

    Étienne André

  2. University of Twente, Enschede, The Netherlands

    Mariëlle Stoelinga

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Syifa’ul Mufid, M., Adzkiya, D., Abate, A. (2019). Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions. In: André, É., Stoelinga, M. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2019. Lecture Notes in Computer Science(), vol 11750. Springer, Cham. https://doi.org/10.1007/978-3-030-29662-9_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-29662-9_9

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-29661-2

  • Online ISBN: 978-3-030-29662-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation