This toolbox is used to generate finite abstractions of autonomous Max-Plus-Linear (MPL) systems 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 system. 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 C++ language. The abstraction procedure runs in C++. 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 JAVA language, we suggest you to try VeriSiMPL version 2.0 which is fully based on JAVA.

If you are more familiar with MATLAB language, we suggest you to try VeriSiMPL version 1.4 which is fully based on MATLAB.

Features

  • 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)

Project Samples

Project Activity

See All Activity >

Categories

Mathematics

License

GNU General Public License version 3.0 (GPLv3)

Follow VeriSiMPL

VeriSiMPL Web Site

nel_h2
Gen AI apps are built with MongoDB Atlas Icon
Gen AI apps are built with MongoDB Atlas

Build gen AI apps with an all-in-one modern database: MongoDB Atlas

MongoDB Atlas provides built-in vector search and a flexible document model so developers can build, scale, and run gen AI apps without stitching together multiple databases. From LLM integration to semantic search, Atlas simplifies your AI architecture—and it’s free to get started.
Start Free

Additional Project Details

Intended Audience

Education, Engineering, Science/Research

Programming Language

Java, MATLAB

Related Categories

MATLAB Mathematics Software, Java Mathematics Software

Registered

2013-01-07