MATISSE
MATISSE (Metrics for Approximate TransItion Systems Simulation and Equivalence) is a free MATLAB toolbox for safety verification and reachable set computation of large dimensional, constrained linear systems. The main functionalities of MATISSE are :
- Given a constrained linear system, the toolbox computes a lower dimensional approximation of the system, and provides error bounds for the precision of the approximation.
- The computation of a bisimulation function between a constrained linear system and its projection.
- The computation of the reachable sets of a constrained linear system using zonotope methods.
Matisse is based on the framework of abstracting linear systems using approximate bisimulation relations. Approximate bisimulation relations aim in capturing the most significant characteristics of a system dynamics and neglect less important ones. The degree of approximation is given by the precision of the approximate bisimulation. This precision notably provides a bound of the distance between the trajectories of a system and of its abstraction.
Approximate bisimulation based abstraction is particularly useful for the safety verification problem which consists in checking whether the intersection of the reachable set of the system with an unsafe set is empty or not. If we can check that the distance of the unsafe set to the reachable set of the abstraction of the system is greater than the precision of the approximate bisimulation then it follows that the original system is safe. The more robustly safe a system, the more approximations are possible which confirms the intuitive fact that the verification of robustly safe systems should be easier.
Downloads:
Download MATISSE
Version : 1.0
Requirements :
- Windows 2000/XP.
- MATLAB version 6.5 (or higher).
- The Multi Parametric Toolbox (MPT) by M. Kvasnica and P. Grieder and M. Baotic.
- YALMIP by Johan Lofberg. Also distributed with the MPT.
- SEDUMI by Jos F. Sturm. Also distributed with the MPT.
Date added : October 12, 2005
Documentation:
- Approximate Bisimulations Relations for Constrained Linear Systems. (pdf)
Antoine Girard and George J. Pappas, Technical Report MS-CIS-05-19, Dept. of CIS, University of Pennsylvania, September 2005. - Approximation Metrics for Discrete and Continuous Systems. (pdf)
Antoine Girard and George J. Pappas, Technical Report MS-CIS-05-10, Dept. of CIS, University of Pennsylvania, Submitted May 2005. - Approximate Bisimulations for Constrained Linear Systems. (pdf)
Antoine Girard and George J. Pappas, to appear in 44th IEEE Conference on Decision and Control and European Control Conference, December 2005. - Approximate Bisimulations for Nonlinear Dynamical Systems. (pdf)
Antoine Girard and George J. Pappas, to appear in 44th IEEE Conference on Decision and Control and European Control Conference, December 2005.
Developers:
Antoine Girard, Department of Electrical and Systems Engineering, University of Pennsylvania.
A. Agung Julius, Department of Electrical and Systems Engineering, University of Pennsylvania.
George J. Pappas, Department of Electrical and Systems Engineering, University of Pennsylvania.
About the painter (quoted from Nancy Doyle Fine Art):
"Matisse began with still lifes and interiors which still contained some observation of nature in the drawing of objects, with some 'flattening' of forms and of the canvas surface. As he matured as an artist, the forms became more and more simplified, and the images became less concerned with 'correct' drawing. Eventually, his images appear to have been only cursorily drawn and painted - just the essential parts were distilled from the image. There was no use of linear perspective to indicate spatial depth in this new painting; on the contrary, Matisse used his curvilinear forms and bold decorative patterns to emphasize the flatness of the canvas surface. There was also no blending of colors - they were placed flatly against one another, avoiding the 'soft' look of blended color and the 'natural' look of this method of depicting three dimensions."