Document Open Access Logo

SMT-Based Model Checking of Max-Plus Linear Systems

Authors Muhammad Syifa'ul Mufid , Andrea Micheli , Alessandro Abate , Alessandro Cimatti

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2021.22.pdf
  • Filesize: 1.93 MB
  • 20 pages

Document Identifiers

Author Details

Muhammad Syifa'ul Mufid
  • Department Computer Science, University of Oxford, UK
Andrea Micheli
  • Fondazione Bruno Kessler, Trento, Italy
Alessandro Abate
  • Department Computer Science, University of Oxford, UK
Alessandro Cimatti
  • Fondazione Bruno Kessler, Trento, Italy

Cite AsGet BibTex

Muhammad Syifa'ul Mufid, Andrea Micheli, Alessandro Abate, and Alessandro Cimatti. SMT-Based Model Checking of Max-Plus Linear Systems. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 22:1-22:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CONCUR.2021.22

Abstract

Max-Plus Linear (MPL) systems are an algebraic formalism with practical applications in transportation networks, manufacturing and biological systems. MPL systems can be naturally modeled as infinite-state transition systems, and exhibit interesting structural properties (e.g. periodicity or steady state), for which analysis methods have been recently proposed. In this paper, we tackle the open problem of specifying and analyzing user-defined temporal properties for MPL systems. We propose Time-Difference LTL (TDLTL), a logic that encompasses the delays between the discrete-time events governed by an MPL system, and characterize the problem of model checking TDLTL over MPL. We propose a family of specialized algorithms leveraging the periodic behaviour of an MPL system. We prove soundness and completeness, showing that the transient and cyclicity of the MPL system induce a completeness threshold for the verification problem. The algorithms are cast in the setting of SMT-based verification of infinite-state transition systems over the reals, with variants depending on the (incremental vs upfront) computation of the bound, and on the (explicit vs implicit) unrolling of the transition relation. Our comprehensive experiments show that the proposed techniques can be applied to MPL systems of large dimensions and on general TDLTL formulae, with remarkable performance gains against a dedicated abstraction-based technique and a translation to the nuXmv symbolic model checker.

Subject Classification

ACM Subject Classification
  • Theory of computation → Verification by model checking
Keywords
  • Max-Plus Linear Systems
  • Satisfiability Modulo Theory
  • Model Checking
  • Linear Temporal Logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Alessandro Abate, Alessandro Cimatti, Andrea Micheli, and Muhammad Syifa'ul Mufid. Computation of the transient in max-plus linear systems via SMT-solving. In Nathalie Bertrand and Nils Jansen, editors, Formal Modeling and Analysis of Timed Systems, pages 161-177, Cham, 2020. Springer International Publishing. Google Scholar
  2. Dieky Adzkiya, Bart De Schutter, and Alessandro Abate. Finite abstractions of max-plus-linear systems. IEEE Transactions on Automatic Control, 58(12):3039-3053, 2013. Google Scholar
  3. Dieky Adzkiya, Bart De Schutter, and Alessandro Abate. Backward reachability of autonomous max-plus-linear systems. IFAC Proceedings Volumes, 47(2):117-122, 2014. Google Scholar
  4. Dieky Adzkiya, Bart De Schutter, and Alessandro Abate. Forward reachability computation for autonomous max-plus-linear systems. In Erika Abraham and Klaus Havelund, editors, Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), volume 8413 of LNCS, pages 248-262. Springer, 2014. Google Scholar
  5. Dieky Adzkiya, Bart De Schutter, and Alessandro Abate. Computational techniques for reachability analysis of max-plus-linear systems. Automatica, 53:293-302, 2015. Google Scholar
  6. Mohsen Alirezaei, Ton JJ van den Boom, and Robert Babuska. Max-plus algebra for optimal scheduling of multiple sheets in a printer. In Proc. 31st American Control Conference (ACC), 2012, pages 1973-1978, June 2012. Google Scholar
  7. François Baccelli, Guy Cohen, Geert Jan Olsder, and Jean-Pierre Quadrat. Synchronization and linearity: an algebra for discrete event systems. John Wiley & Sons Ltd, 1992. Google Scholar
  8. Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008. Google Scholar
  9. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 825-885. IOS Press, 2009. URL: https://doi.org/10.3233/978-1-58603-929-5-825.
  10. Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu. Symbolic model checking without BDDs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 193-207. Springer, 1999. URL: https://doi.org/10.1007/3-540-49059-0_14.
  11. Armin Biere, Alessandro Cimatti, Edmund M Clarke, Ofer Strichman, Yunshan Zhu, et al. Bounded model checking. Advances in Computers, 58(11):117-148, 2003. Google Scholar
  12. Armin Biere, Keijo Heljanko, Tommi Junttila, Timo Latvala, and Viktor Schuppan. Linear encodings of bounded LTL model checking. Logical Methods in Computer Science, 2(5):1-64, 2006. URL: https://doi.org/10.2168/LMCS-2(5:5)2006.
  13. J-L Bouquard, Christophe Lenté, and J-C Billaut. Application of an optimization problem in max-plus algebra to scheduling problems. Discrete Applied Mathematics, 154(15):2064-2079, 2006. Google Scholar
  14. Chris A Brackley, David S Broomhead, M Carmen Romano, and Marco Thiel. A max-plus model of ribosome dynamics during mRNA translation. Journal of Theoretical Biology, 303:128-140, 2012. Google Scholar
  15. Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. The nuxmv symbolic model checker. In International Conference on Computer Aided Verification, pages 334-342. Springer, 2014. Google Scholar
  16. Bernadette Charron-Bost, Matthias Függer, and Thomas Nowak. New transience bounds for max-plus linear systems. Discrete Applied Mathematics, 219:83-99, 2017. Google Scholar
  17. Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. IC3 modulo theories via implicit predicate abstraction. In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, pages 46-61. Springer, 2014. Google Scholar
  18. Edmund Clarke, Orna Grumberg, Muralidhar Talupur, and Dong Wang. Making predicate abstraction efficient. In Proc. International Conference on Computer Aided Verification 2003 (CAV'03), pages 126-140. Springer, 2003. Google Scholar
  19. Edmund Clarke, Daniel Kroening, Joël Ouaknine, and Ofer Strichman. Completeness and complexity of bounded model checking. In International Workshop on Verification, Model Checking, and Abstract Interpretation, pages 85-96. Springer, 2004. URL: https://doi.org/10.1007/978-3-540-24622-0_9.
  20. J-P Comet. Application of max-plus algebra to biological sequence comparisons. Theoretical computer science, 293(1):189-217, 2003. Google Scholar
  21. RA Cuninghame-Green and P Butkovic. Generalised eigenproblem in max-algebra. In International Workshop on Discrete Event Systems, pages 236-241. IEEE, 2008. Google Scholar
  22. Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, and Sergio Mover. Infinite-state liveness-to-safety via implicit abstraction and well-founded relations. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I, volume 9779 of Lecture Notes in Computer Science, pages 271-291. Springer, 2016. Google Scholar
  23. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), volume 4963 of LNCS, pages 337-340. Springer, 2008. Google Scholar
  24. Bart De Schutter. On the ultimate behavior of the sequence of consecutive powers of a matrix in the max-plus algebra. Linear Algebra and its Applications, 307(1-3):103-117, 2000. Google Scholar
  25. David L Dill. Timing assumptions and verification of finite-state concurrent systems. In J. Sifakis, editor, Intl. Conf. on Computer Aided Verification (CAV'89), volume 407 of Lecture Notes in Computer Science, pages 197-212, Hiedelberg, 1989. Springer. Google Scholar
  26. Alexandre Duret-Lutz, Alexandre Lewkowicz, Amaury Fauchille, Thibaud Michaud, Etienne Renault, and Laurent Xu. Spot 2.0 - a framework for ltl and omega-automata manipulation. In International Symposium on Automated Technology for Verification and Analysis, pages 122-129. Springer, 2016. Google Scholar
  27. Susanne Graf and Hassen Saïdi. Construction of abstract state graphs with PVS. In In Proc. International Conference on Computer Aided Verification (CAV'97), pages 72-83. Springer, 1997. Google Scholar
  28. Wilhemus Heemels, Bart De Schutter, and Alberto Bemporad. Equivalence of hybrid dynamical models. Automatica, 37(7):1085-1091, July 2001. Google Scholar
  29. Bernd Heidergott, Geert Jan Olsder, and Jacob Van der Woude. Max Plus at work: modeling and analysis of synchronized systems: a course on Max-Plus algebra and its applications. Princeton University Press, 2014. Google Scholar
  30. Aleksey Imaev and Robert P Judd. Hierarchial modeling of manufacturing systems using max-plus algebra. In Proc. American Control Conference, 2008, pages 471-476, June 2008. Google Scholar
  31. Daniel Kroening, Joël Ouaknine, Ofer Strichman, Thomas Wahl, and James Worrell. Linear completeness thresholds for bounded model checking. In International Conference on Computer Aided Verification, pages 557-572. Springer, 2011. Google Scholar
  32. Glenn Merlet, Thomas Nowak, and Sergei Sergeev. Weak CSR expansions and transience bounds in max-plus algebra. Linear Algebra and its Applications, 461:163-199, 2014. Google Scholar
  33. M.S. Mufid, D. Adzkiya, and A. Abate. Tropical abstractions of max-plus linear systems. In D.N. Jansen and P. Prabhakar, editors, Int. Conf. Formal Modeling and Analysis of Timed Systems (FORMATS'18), pages 271-287. Springer, 2018. Google Scholar
  34. Muhammad Syifa’ul Mufid, Dieky Adzkiya, and Alessandro Abate. Bounded model checking of max-plus linear systems via predicate abstractions. In International Conference on Formal Modeling and Analysis of Timed Systems, pages 142-159. Springer, 2019. Google Scholar
  35. Thomas Nowak and Bernadette Charron-Bost. An overview of transience bounds in max-plus algebra. Tropical and Idempotent Mathematics and Applications, 616:277-289, 2014. Google Scholar
  36. Gerardo Soto Y Koelemeijer. On the behaviour of classes of min-max-plus systems. PhD thesis, Delft University of Technology, 2003. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact