VeriSiMPL Files

% Verification via biSimulations of MPL models (VeriSiMPL) Toolbox
% Version 1.4 (10-Apr-2014)

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

Main bibliographical references:
1) D. Adzkiya and A. Abate,
   ``VeriSiMPL: Verification via biSimulations of MPL Models''
   In Proceedings of the 10th Quantitative Evaluation of Systems
   volume 8054 of Lecture Notes in Computer Science, pages 253-256, Springer, Heidelberg
   Buenos Aires, September 2013.
2) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Finite Abstractions of Max-Plus-Linear Systems''
   IEEE Transactions on Automatic Control 58(12), pages 3039-3053, December 2013.
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''
   In Proceedings of the 31st American Control Conference, pages 721-726
   Montreal - CA, June 2012.
2) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Finite Abstractions of Nonautonomous Max-Plus-Linear Systems''
   In Proceedings of the 32nd American Control Conference, pages 4387-4392
   Washington, June 2013.
3) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Forward Reachability Computation for Autonomous Max-Plus-Linear Systems''
   In Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems
   volume 8413 of Lecture Notes in Computer Science, pages 248-262, Springer, Heidelberg
   Grenoble, April 2014.
4) D. Adzkiya, B. De Schutter, and A. Abate,
   ``Backward Reachability of Autonomous Max-Plus-Linear Systems''
   Proceedings of the 12th IFAC - IEEE International Workshop on Discrete Event Systems, May 2014, Paris.

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.

This toolbox can also be used for reachability computations of
autonomous and nonautonomous MPL models.
Forward and backward reachability are equally supported.
The user can compute either reach tube or reach set.

There is also a function to export an autonomous MPL system to
a piecewise affine (PWA) system in multi-parametric toolbox (MPT) version 2.
This enables the use of features in MPT to PWA representation of MPL system.

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

This toolbox consists of the following main files: 

mpl2pwa_part.m              - generate partitions
ts_trans.m                  - determine transitions (autonomous models)
ts_label.m                  - compute transition labels (autonomous models)
ts_refine.m                 - refinement procedure to obtain a deterministic transition system (autonomous models)
mplnon2pwa_part.m           - generate partitions
tsnon_trans.m               - determine transitions (nonautonomous models)
tsnon_label.m               - compute transition labels (nonautonomous models)
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)
mpl2pwa.m                   - generate piecewise-affine systems
mpl2pwa_refine.m            - refine regions of piecewise-affine systems to obtain a partition
ts2graphviz.m               - export the transition system to graphviz code (dot)
mpl2pwa_mpt.m               - generate PWA system in MPT version 2 structure
mpl_reachset_back.m         - compute backward reach set of autonomous models
mpl_reachset_for.m          - compute forward reach set of autonomous models
mpl_reachtube_back.m        - compute backward reach tube of autonomous models
mpl_reachtube_for.m         - compute forward reach tube of autonomous models
mplnon_reachtube_back.m     - compute backward reach tube of nonautonomous models
mplnon_reachtube_for.m      - compute forward reach tube of nonautonomous models
maxpl2ts_demo.m             - GUI for abstraction of autonomous max-plus-linear systems
maxpl_absver_demo.m         - GUI for abstraction and verification of autonomous max-plus-linear systems
maxpl_reachfor_demo.m       - GUI for forward reachability of autonomous max-plus-linear systems (NEW FEATURE IN THIS VERSION)

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.