This toolbox is used to generate finite abstractions of autonomous
Max-Plus-Linear (MPL) models over R^n. Abstractions are
characterized as finite-state Labeled Transition Systems (LTS).
The LTS finite abstractions are shown to either simulate or to bisimulate
the original MPL model. LTS models are to be verified against given
specifications expressed as formulae in Linear Temporal Logic (LTL) and
Computation Tree Logic (CTL). The toolbox intends to leverage the NuSMV model checker.
Models are to be expressed in the JAVA language.
The abstraction procedure runs in JAVA.
The generated LTS is exported to the NuSMV language.
As such, it can be fed, along with a specification of interest, to the NuSMV model checker.
If you are more familiar with MATLAB models, we suggest you to try VeriSiMPL version 1.4.
- Generate finite-state LTS abstraction from an MPL system using list and tree data structure
- Generate Piece-wise Affine representation from an MPL system
- Verify an MPL system against an LTL or CTL formula
- Visualize the TS in Graphviz (Version 1.4)
- Export autonomous model to PWA system in MPT structure (Version 1.4)
- Reachability analysis of MPL systems (Version 1.4)
- GUI for abstraction and verification of autonomous MPL systems (Version 1.4)
- GUI for forward reachability of autonomous MPL systems (Version 1.4)
Be the first to post a review of VeriSiMPL!