\texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems

DOI10.1007/S10626-015-0218-XMaRDI QIDQ262437zbMATH OpenOpenAlexWikidataFDO

Authors Dieky Adzkiya, Yining Zhang, Alessandro Abate

Publication date 29 March 2016

Published in Discrete Event Dynamic Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10626-015-0218-x

zbMATH Keywords

model checkingbisimulationsdifference-bound matricesdiscrete-event systemsmax-plus algebramodel abstractionspiece-wise affine systemstransition systems

Mathematics Subject Classification ID

Applications of graph theory (05C90) Discrete event control/observation systems (93C65) Software, source code, etc. for problems pertaining to systems and control theory (93-04)

Recommendations

• Bounded model checking of max-plus linear systems via predicate abstractions
• Tropical abstractions of MAX-plus linear systems
• Computational techniques for reachability analysis of Max-Plus-Linear systems
• Stable model predictive control for constrained max-plus-linear systems
• Stabilization of max-plus-linear systems using model predictive control: the unconstrained case

Cites work

• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 627763 (Why is no real title available?)
• scientific article; zbMATH DE number 1903365 (Why is no real title available?)
• scientific article; zbMATH DE number 5018129 (Why is no real title available?)
• scientific article; zbMATH DE number 5585443 (Why is no real title available?)
• A MAX-plus model of ribosome dynamics during mRNA translation
• Bisimilar linear systems.
• Branching Programs and Binary Decision Diagrams
• Computational techniques for reachability analysis of Max-Plus-Linear systems
• Duality between invariant spaces for max-plus linear discrete event systems
• Equivalence of hybrid dynamical models
• Explicit formulas for the solutions of piecewise linear networks
• Finite Abstractions of Max-Plus-Linear Systems
• Formal Analysis of Discrete-Time Piecewise Affine Systems
• Formal analysis of piecewise affine systems through formula-guided refinement
• Max-Plus $(A,B)$-Invariant Spaces and Control of Timed Discrete-Event Systems
• Minimax algebra
• Model predictive control for max-plus-linear discrete event systems
• Nonlinear regulation: The piecewise linear approach
• O-minimal hybrid systems.
• Observability and controllability of piecewise affine and hybrid systems
• On a routing problem
• On the control of max-plus linear system subject to state restriction
• On the ultimate behaviour of the sequence of consecutive powers of a matrix in the max-plus algebra

Cited in

(4)

• Bounded model checking of max-plus linear systems via predicate abstractions
• Tropical abstractions of MAX-plus linear systems
• Computational techniques for reachability analysis of Max-Plus-Linear systems
• Conditional reachability of uncertain max plus linear systems

Describes a project that uses

Uses Software

• Algorithm 97
• VeriSIMPL
• FaPAS
• Maxplus
• NuSMV
• SPIN

This page was built for publication: \texttt{VeriSIMPL 2}: an open-source software for the verification of max-plus-linear systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q262437)