About SpaceEx
The verification of continuous and hybrid systems is a challenging problem, and various approaches are currently being investigated to overcome the complexities of representing and computing with continuous sets of states. Since verification problems are generally undecidable for such systems, experimental results are vital for evaluating and developing new ideas.
The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safetyverification. While these methods are based on different representations (polyhedra, zonotopes) and are tailored to different dynamics (piecewise constant, affine, multi-affine, nonlinear), they have several things in common: The model is a composition of hybrid automata (including extensions such as hierarchy and templates). Basic components of analysis algorithms are post- and pre-operators in various flavors. The reachable states are explored using symbolic states. They require basic infrastructure such as parsing input and visualizing states.
Our framework provides the common components and developers can substitute components as well as easily add new functionality. We extensively make use of polymorphism to enable the development of heterogeneous analysis methods, such as using different set representations in different parts of the state space or at different levels of refinement, or combining symbolic computations with simulation. In general, our framework allows all set operators (union, intersection, etc.) to return a set of a different type. The development of the framework was spawned by recent progress in finding efficient data structures and algorithms for reachability computation. Building on our experience with PHAVer, our goal is to improve and extend a particular type of reachability computation, allowing tool developers to substitute different implementations for components where suitable. These restrictions enable us to tune the implementation to suit our specific application.
A conference presentation on SpaceEx is available here.
