Top

Published in:

2019 | OriginalPaper | Chapter

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

Authors : Muhammad Syifa’ul Mufid, Dieky Adzkiya, Alessandro Abate

Published in: Formal Modeling and Analysis of Timed Systems

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Piecewise Robust Barrier Tubes for Nonlinear Hybrid Systems with Uncertainty

next chapter Reachability Analysis for High-Index Linear Differential Algebraic Equations

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

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

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

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

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.2273299MathSciNetCrossRefMATH

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-xMathSciNetCrossRefMATH

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_4CrossRefMATH

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

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

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.378846CrossRef

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_14CrossRef

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

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)2006MathSciNetCrossRefMATH

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.007MathSciNetCrossRefMATH

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_29CrossRef

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_15CrossRef

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_14CrossRef

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_9CrossRefMATH

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.f3CrossRefMATH

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_7CrossRef

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.186051CrossRef

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-2MathSciNetCrossRefMATH

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_16CrossRef

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-6MathSciNetCrossRefMATH

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_10CrossRef

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-0CrossRefMATH

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)

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_10CrossRef

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)

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_25CrossRefMATH

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_16CrossRefMATH

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

Title: Bounded Model Checking of Max-Plus Linear Systems via Predicate Abstractions
Authors: Muhammad Syifa’ul Mufid
Dieky Adzkiya
Alessandro Abate
Publisher: Springer International Publishing
Book: Formal Modeling and Analysis of Timed Systems
Print ISBN: 978-3-030-29661-2

Electronic ISBN: 978-3-030-29662-9

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-29662-9_9

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner