SMT-based model checking of max-plus linear systems
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...
| Auteurs principaux: | , , , |
|---|---|
| Format: | Conference item |
| Langue: | English |
| Publié: |
Schloss Dagstuhl
2021
|
| _version_ | 1826260021054275584 |
|---|---|
| author | Mufid, MSU Micheli, A Abate, A Cimatti, A |
| author_facet | Mufid, MSU Micheli, A Abate, A Cimatti, A |
| author_sort | Mufid, MSU |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T18:59:01Z |
| format | Conference item |
| id | oxford-uuid:12e1475f-937f-4ceb-82dd-c27b509b8d4d |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T18:59:01Z |
| publishDate | 2021 |
| publisher | Schloss Dagstuhl |
| record_format | dspace |
| spelling | oxford-uuid:12e1475f-937f-4ceb-82dd-c27b509b8d4d2022-03-26T10:10:30ZSMT-based model checking of max-plus linear systemsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:12e1475f-937f-4ceb-82dd-c27b509b8d4dEnglishSymplectic ElementsSchloss Dagstuhl2021Mufid, MSUMicheli, AAbate, ACimatti, AMax-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. |
| spellingShingle | Mufid, MSU Micheli, A Abate, A Cimatti, A SMT-based model checking of max-plus linear systems |
| title | SMT-based model checking of max-plus linear systems |
| title_full | SMT-based model checking of max-plus linear systems |
| title_fullStr | SMT-based model checking of max-plus linear systems |
| title_full_unstemmed | SMT-based model checking of max-plus linear systems |
| title_short | SMT-based model checking of max-plus linear systems |
| title_sort | smt based model checking of max plus linear systems |
| work_keys_str_mv | AT mufidmsu smtbasedmodelcheckingofmaxpluslinearsystems AT michelia smtbasedmodelcheckingofmaxpluslinearsystems AT abatea smtbasedmodelcheckingofmaxpluslinearsystems AT cimattia smtbasedmodelcheckingofmaxpluslinearsystems |