License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2021.22
URN: urn:nbn:de:0030-drops-143993
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14399/
Go to the corresponding LIPIcs Volume Portal

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

SMT-Based Model Checking of Max-Plus Linear Systems

pdf-format:
LIPIcs-CONCUR-2021-22.pdf (2 MB)

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.

BibTeX - Entry

@InProceedings{mufid_et_al:LIPIcs.CONCUR.2021.22,
  author =	{Mufid, Muhammad Syifa'ul and Micheli, Andrea and Abate, Alessandro and Cimatti, Alessandro},
  title =	{{SMT-Based Model Checking of Max-Plus Linear Systems}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{22:1--22:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14399},
  URN =		{urn:nbn:de:0030-drops-143993},
  doi =		{10.4230/LIPIcs.CONCUR.2021.22},
  annote =	{Keywords: Max-Plus Linear Systems, Satisfiability Modulo Theory, Model Checking, Linear Temporal Logic}
}

Keywords: Max-Plus Linear Systems, Satisfiability Modulo Theory, Model Checking, Linear Temporal Logic
Collection: 32nd International Conference on Concurrency Theory (CONCUR 2021)
Issue Date: 2021
Date of publication: 13.08.2021

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI