VeriSiMPL Files

% Verification via biSimulations of MPL models (VeriSiMPL) Toolbox
% Version 1.2 (14-Jan-2013)

Webpages:
http://sourceforge.net/projects/verisimpl
http://www.dcsc.tudelft.nl/~aabate/VeriSiMPL.html

Authors:
Dieky Adzkiya and Alessandro Abate

Emails contacts:
{d.adzkiya,a.abate}@tudelft.nl

Mail contact: 
Delft Center for Systems and Control
TU Delft - Delft University of Technology
Mekelweg 2, 2628CD Delft, 
The Netherlands

Bibliographical references: 
D. Adzkiya, B. De Schutter, and A. Abate, 
``Abstraction and Verification of Autonomous Max-Plus-Linear Systems''
Proceedings of the 31st American Control Conference, June 2012, Montreal - CA. 
G. Holzmann, 
``The SPIN Model Checker''
Addison-Wesley, 2003. 

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.

Installation
============

This toolbox consists of the following main files: 

maxpl2ts_part.m          - generate partitions
maxpl2ts_trans.m         - determine transitions
maxpl2ts_label.m         - compute transition labels
maxpl2ts_refine.m        - refinement procedure to obtain a deterministic transition system
maxplnon2ts_part.m       - generate partitions
maxplnon2ts_trans.m      - determine transitions
maxplnon2ts_label.m      - compute transition labels
ts2spin_state.m          - generate spin code for verification over state labels (both models)
ts2spin_trans.m          - generate spin code for verification over transition labels (autonomous models)
tsnon2spin_trans.m       - generate spin code for verification over transition labels (nonautonomous models)
maxpl2pwa.m              - generate piecewise-affine systems
maxpl2pwa_refine.m       - refine regions of piecewise-affine systems to obtain a partition
ts2graphviz.m            - export the transition system to graphviz code (dot)
run_examples.m           - run examples given in every file

In order to use this toolbox, set a Matlab path to the "VeriSiMPL/" directory.
This toolbox has been successfully tested with Matlab R2009b, R2010b, R2011a, R2011b, R2012b.

Support
=======

There is no support! This toolbox is made freely available in the hope 
that you find it useful in solving whatever problems you have to hand.
We are happy to correspond with people who have found genuine bugs. 
If you have any questions or comments, or you observe buggy behavior 
of this toolbox, please send your reports by email to the authors.