Major Update: SpaceEx v0.9.8

The latest update of SpaceEx introduces major improvements and new features.

• Proper treatment of algebraic equations,
• block diagrams in the model editor, 
• overall better performance, and 
• important bug fixes.

Version 0.9.8 is now available for download, including images for VMWare and VirtualBox. For details on the new algorithms, see the following publications:

• A. Donze, G. Frehse. Modular, Hierarchical Models of Control Systems in SpaceEx. ECC 2013.
• G. Frehse, R. Kateja, C. Le Guernic. Flowpipe Approximation and Clustering in Space-Time. HSCC 2013.

A summary of major changes follows.

Algebraic Equations

Algebraic variables are now eliminated as much as possible. This is done separately for each location, so that a variable may be used as a state variable in one location and as an algebraic variable in another. For example, when a PI-Controller is "off" in a location, it suffices to simply not mention it's state variable in that location, or to assign its value in an algebraic equation.

Fig. 1: In this example, e_int is a state variable only in the location on the left

In complex models, this can significantly reduce the dimension of the ODEs handled by the analysis, and therefore marked increase in speed. The elimination of algebraic variables takes place only once per location, so little overhead is involved.

Block Diagrams

The model editor now supports block diagrams, in which components are connected just like in Matlab/Simulink or Modelica/Dymola. Control systems can be modeled quickly from standard components such as PID, integrators, gain, switches, constants, etc.

Fig. 2: The block diagram of a standard control system in the SpaceEx Model Editor

Performance Improvements

SpaceEx has gotten faster through improved preprocessing of models (including eliminating DAEs and redundant inequalities) and various minor enhancements such as caching of matrix exponentials. The STC algorithm has been significantly improved and is now often both faster and more precise than the LGG algorithm.
The STC scenario now features relative as well as absolute error tolerances. Error messages and log output have been improved.

Important Bug Fixes

A total of 45 bugs were fixed since v0.9.7b, including three major bugs that can lead to wrong results:

• Transitions without labels could erroneously synchronize under certain circumstances.
• The composition operator would sometimes produce erroneous inhomogeneous coefficients of ODEs.
• Constraints would erroneously be considered redundant and be dropped from state predicates.

The SpaceEx team is very grateful to all users who submitted bug reports and examples.

Known Issues

For now, only state variables can be part of the output; algebraic variables will generally be reported as unbounded. This is because the inclusion of algebraic constraints could lead to severely degraded performance of the graphical output. Better solutions are under investigation.