Tools

VeriSiMPL

Verification via biSimulations of Max-Plus-Linear models

Description

This toolbox is used to generate finite abstractions of autonomous and nonautonomous 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). The toolbox intends to leverage the SPIN model checker.

Models are to be expressed in MATLAB language. The abstraction procedure runs in MATLAB. The generated LTS is exported to the PROMELA. As such, it can be fed, along with a specification of interest, to the SPIN model checker.

Features

  • Generate finite-state LTS abstraction from a MPL model
  • Generate Piece-Wise Affine representation from a MPL model
  • Visualize the TS in Graphviz

 

MRMC

Markov Reward Model Checker

Description
In recent years, RWTHA has developed the probabilistic model checker MRMC. It supports the verication of continuous- and discrete-time Markov chains, as well as reward extensions thereof, against branching-time temporal logic specications. Recently, prototypical spin-os have been developed for verifying CTMCs against (linear-time) timed automata specifications, as well as, extensions towards analysing continuous-time Markov decision processes (called IMCA).

 

AVACS SiSAT Solver

Description
OFFIS has cooperated with the transregional research center AVACS (SFB/TR 14 Automatic Verication and Analysis of Complex Systems) in the development of the prototypic model checker ProHVer, a front-end to PRISM abstracting probabilistic hybrid automata to nite-state Markov decision processes. Building on the publicly available Stochastic-SAT-Modulo-Theory (SSMT) solver SiSAT of the AVACS project, OFFIS has furthermore developed a completely new SSMT solving technique incorporating randomized sampling techniques and implemented this in a solver prototype that will be made available after stabilization.

 

announcements

VeriSiMPL Toolbox
Verification via biSimulations of Max-Plus-Linear models. This toolbox is used to generate finite abstractions of autonomous and nonautonomous Max-Plus-Linear (MPL) models over R^n. Alessandro Abate & Dieky Adzkiya (TU Delft).