VeriSiMPL Files

% Verification via biSimulations of MPL models (VeriSiMPL) Toolbox
% Version 1.1 (14-Aug-2012)

Webpage: 
http://www.dcsc.tudelft.nl/~aabate/VeriSiMPL.html

Contacts: 
Dieky Adzkiya and Alessandro Abate
Emails: 
{d.adzkiya,a.abate}@tudelft.nl 

Mail: 
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: 

VeriSiMPL/maxpl2ts_part.m      - generate partitions
VeriSiMPL/maxpl2ts_trans.m     - determine transitions
VeriSiMPL/maxpl2ts_label.m     - compute transition labels
VeriSiMPL/maxpl2ts_refine.m    - refinement procedure
VeriSiMPL/maxplnon2ts_part.m   - generate partitions
VeriSiMPL/maxplnon2ts_trans.m  - determine transitions
VeriSiMPL/maxplnon2ts_label.m  - compute transition labels
VeriSiMPL/ts2spin_state.m      - generate spin code for verification over state labels (both models)
VeriSiMPL/ts2spin_trans.m      - generate spin code for verification over transition labels (autonomous models)
VeriSiMPL/tsnon2spin_trans.m   - generate spin code for verification over transition labels (nonautonomous models)
VeriSiMPL/maxpl2pwa.m          - generate piecewise-affine systems
VeriSiMPL/ts2graphviz.m        - export the transition system to graphviz code (dot)

In order to use this toolbox, set a Matlab path to the "VeriSiMPL/" directory.
This toolbox has been successfully tested with Matlab 7.14(R2012a) on Linux and Windows platforms.

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.