Bounded model checking of max-plus linear systems via predicate abstractions
From MaRDI portal
Publication:2176702
DOI10.1007/978-3-030-29662-9_9zbMATH Open1434.68302arXiv1907.03564OpenAlexW2970341587MaRDI QIDQ2176702FDOQ2176702
Dieky Adzkiya, Muhammad Syifa'ul Mufid, Alessandro Abate
Publication date: 5 May 2020
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.
Full work available at URL: https://arxiv.org/abs/1907.03564
Recommendations
- \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems
- Tropical abstractions of MAX-plus linear systems
- Stable model predictive control for constrained max-plus-linear systems
- Predicate abstraction for dense real-time systems
- Computational techniques for reachability analysis of Max-Plus-Linear systems
Cited In (2)
This page was built for publication: Bounded model checking of max-plus linear systems via predicate abstractions
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2176702)
