VeriSiMPL Files

% Verification via biSimulations of MPL models (VeriSiMPL) Toolbox
% Version 1.3 (9-Sep-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
alessandro.abate@cs.ox.ac.uk

Mail contacts: 
1) Delft Center for Systems and Control
   TU Delft - Delft University of Technology
   Mekelweg 2, 2628CD Delft, 
   The Netherlands
2) Department of Computer Science
   University of Oxford
   Wolfson Building, Parks Road, Oxford, OX1 3QD,
   United Kingdom

Bibliographical references:
1) D. Adzkiya and A. Abate,
   ``VeriSiMPL: Verification via biSimulations of MPL Models''
   Proceedings of the 10th Quantitative Evaluation of Systems, Aug 2013, Buenos Aires.
2) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Finite Abstractions of Max-Plus-Linear Systems''
   Accepted in IEEE Transactions on Automatic Control.
3) G. Holzmann, 
   ``The SPIN Model Checker''
   Addison-Wesley, 2003. 

Additional bibliographical references:
1) 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.
2) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Finite Abstractions of Nonautonomous Max-Plus-Linear Systems''
   Proceedings of the 32nd American Control Conference, June 2013, Washington.

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)
maxpl2pwa_mpt.m             - generate PWA system in MPT structure
maxpl_reachset_back.m       - compute backward reach set of autonomous models
maxpl_reachset_for.m        - compute forward reach set of autonomous models
maxpl_reachtube_back.m      - compute backward reach tube of autonomous models
maxpl_reachtube_for.m       - compute forward reach tube of autonomous models
maxplnon_reachtube_back.m   - compute backward reach tube of nonautonomous models
maxplnon_reachtube_for.m    - compute forward reach tube of nonautonomous models
maxpl2ts_demo.m             - GUI for abstraction of autonomous models
maxpl_absver_demo.m         - GUI for abstraction and verification of autonomous models

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.