Hybrid Systems
Hybrid systems combining discrete and continuous dynamics arise as mathematical models of various artificial and natural systems, and as an approximation to complex continuous systems. A very important problem in the analysis of the behaviour of hybrid systems is reachability even if it is well-known that for most non-trivial subclasses of hybrid systems this and all interesting verification problems are undecidable. Most of the proved decidability results rely on stringent hypothesis that lead to the existence of a finite and computable partition of the state space into classes of states which are equivalent with respect to reachability.

Polygonal Differential Inclusion Systems
An interesting and still decidable class of hybrid system are SPDIs - 2-dimensional polygonal differential inclusions (also referred to as Polygonal Hybrid Systems and Simple Planar Differential Inclusions). If one imagines a point moving around a two dimensional plane, SPDIs restrict the movement of the point in the following manner. Let the plane be partitioned into a finite number of convex polygonal parts. For each such polygon two vectors indicate the leftmost and rightmost directions the point can move when in that polygon. In [1] it was shown that reachability on an SPDI is decidable.

SPeeDI
The tool SPeeDI [2] is a collection of utilities to manipulate and reason mechanically about SPDIs, completely implemented in 5000 lines of Haskell, a general-purpose, lazy, functional language.

Visualization aids:

To help visualize systems, the tool can generate graphical representations of the SPDI, and particular trajectories and signatures within it.

Information gathering:

SPeeDI calculates edge-to-edge successor function composition and enlists signatures going from one edge to another.

Verification:

The most important facet of the tool suite is that of verification based on the constructive proof of decidability given in [1]. The user may give a restricted initial edge and restricted final edge, and the tool attempts to answer whether the latter is reachable from the former.

Trace generation:

Whenever reachability succeeds SPeeDI generates stripes of feasible trajectories using different strategies and graphical representation of them.

Qualitative analysis

The second version of SPeeDI, (SPeeDI⁺) was augmented with tools to perform qualitative analysis of SPDIs, based on [3]. Typical qualitative questions include: "Are there sink regions which one can never leave once they have been entered?"; "Which are the basins of attraction of such regions?"; "Are there regions in which every point in the region is reachable from any other point in the same region without leaving it?". SPeeDI⁺ calculates a collection of such objects characterizing these sets, which provide useful information about the qualitative behaviour of the hybrid system.

Future Directions
In the near future, we will be releasing a new version of SPeeDI which internally uses an arbitrary precision description of rational numbers, hence eliminating all rounding errors in the analysis. It is hoped that the following theoretical results we have achieved will also be implemented in the toolkit in the future:

Breadth First Search Analysis of SPDIs:

In [4,5,6], we have identified a new algorithm for resolving reachability on SPDIs. The new technique has the advantage of being able to identify shortest traces showing reachability, and also that the technique is almost identical to the standard forward model checking algorithm for discrete systems, hence giving us the opportunity to apply standard optimisations to the algorithm.

Phase Portrait Based State-Space Reduction of SPDIs:

In [8,9], we identified how the results of the qualitative analysis (the phase portrait) of an SPDI can be used to reduce the state space of the SPDI. Since SPeeDI⁺ already calculates the phase portrait of a given SPDI, it is planned that these reductions are applied to improve reachability analysis.

Compositional Analysis of SPDIs for Parallelisation:

The phase portrait of an SPDI can also be used to decompose it into a number of independent reachability problems which can be run in parallel [10]. The technique works best with the breadth-first search algorithm.

SPDI Applications:

The most prominent application of SPDIs is for approximating complex non-linear differential equations on the plane, for which an exact solution is not known. The decidability of SPDI's reachability and of its phase portrait construction would be of invaluable help for the qualitative analysis of such equations. The challenge would be to find an intelligent partition of the plane in order to get an optimal approximation of the equations.

Overview:
SPeeDI⁺ is a toolkit aimed at the analysis of SPDIs. A description of tool can be found in [2]. It includes the following tools:

Information gathering tools:

• getmafs: gives the accumulated MAFs along a given path in an SPDI.
• looptype: shows the type of a loop (STAY, DIE, etc)
• trysig: gives whether a signature satisfies a reachability problem.

Visualisation tools:

• spdi2ps, spdi2fig: Produce a PostScript/fig version of an SPDI.
• sig2ps, sig2fig: Produce a PostScript/fig version of an SPDI together with the path followed by a signature.
• path2fig: Traces the reachable area along a path in a given interval on an SPDI.

Analysis tools:

• showsigs: Show a list of signatures that reachable would analyse.
• reachable: Tries to answer whether a reachability problem is satisfiable.
• simsig: Produce a textual representation of a concrete instance of a signature.
• simsig2fig: Traces the reachable area along a concrete instance of a given signature. Behaves like simsig followed by path2fig.

Qualitative analysis (these tools are available in version 2):

• viability, controllability, invariance: Calculate and show the viability, controllability, invariance kernels (respectively) of a given loop.
• drawkernels: Produces a fig file of the SPDI with all kernels drawn.

SPDI generation tools:

• pspdi2spdi: It is usually convenient to define an SPDI parametrised over some values which can be changed throughout the SPDI file by just tweaking the parameter. This tool allows the user to define constants and macros.
• MSPDI: This is a Perl library to enable the generation of large regular SPDIs. It is, as yet, undocumented, but you can look at the examples included to work out how to use it.

• SPeeDI⁺ (version 2 of SPeeDI): This is the latest version of SPeeDI, which includes phase portrait analysis.
• SPeeDI (version 1.2): An earlier version of SPeeDI.
• Parametrised SPDIs: The script to extract an SPDI file from a parametrised SPDI one.
• MSPDI: This includes the Perl libraries which enable the generation of regular SPDIs, and a directory with a number of examples of its use.