SPeeDI+: A 2 Dimensional Hybrid System Model Checker

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.

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.
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.

SPeeDI Papers
[1] On the Decidability of the Reachability Problem for Planar Differential Inclusions, Eugene Asarin, Gerardo Schneider, and Sergio Yovine, in HSCC'2001, number 2034 in LNCS, pages 89-104, Rome, Italy, 2001. (PDF) (BiBTeX entry)
[2] SPeeDI - A Verification Tool for Polygonal Hybrid Systems, Eugene Asarin, Gordon Pace, Gerardo Schneider and Sergio Yovine, in Computer-Aided Verification (CAV 2002) published in LNCS 2404, Copenhagen, Denmark, 2002. (PDF) (BiBTeX entry)
[3] Towards Computing Phase Portraits of Polygonal Differential Inclusions, Eugene Asarin, Gerardo Schneider, and Sergio Yovine, in HSCC'2002, number 2289 in LNCS, pages 49-61, Stanford, USA, March 2002. (PDF) (BiBTeX entry)
[4] Model Checking Polygonal Differential Inclusions Using Invariance Kernels, Gordon Pace and Gerardo Schneider, in Verification and Model Checking and Abstract Interpretation (VMCAI 2004) to be published in LNCS, Venice, Italy, 2004. (PDF) (BiBTeX entry)
The technical details of the VMCAI'04 paper are available in two technical reports:
[5] A New Breadth-First Search Algorithm for Deciding SPDI Reachability Gordon Pace, Department of Computer Science and AI, University of Malta. Technical Report CSAI2003-01. (PDF) (BiBTeX entry)
[6] Invariance Kernels of Polygonal Differential Inclusions Gerardo Schneider, Department of IT, Uppsala University. Technical Report 2003-042. (PDF) (BiBTeX entry)
[7] Computing Invariance Kernels of Polygonal Hybrid Systems, Gerardo Schneider, Nordic Journal of Computing, 11(2):194-210, 2004.
[8] Static Analysis for State-Space Reduction of Polygonal Hybrid Systems, Gordon Pace and Gerardo Schneider, in Formal Modelling and Analysis of Timed Systems (FORMATS'06), Springer-Verlag LNCS (to appear), Paris, France. 2006. (PDF) (BiBTeX entry)
The above paper with some additional proofs is available as a University of Oslo technical report.
[9] Static Analysis of SPDIs for State-Space Reduction, Gordon Pace and Gerardo Schneider, Technical Report 336, Department of Informatics, University of Oslo, PO Box 1080 Blindern, N-0316 Oslo, Norway. 2006. (PDF) (BiBTeX entry)
[10] A Compositional Algorithm for Parallel Model Checking of Polygonal Hybrid Systems, Gordon Pace and Gerardo Schneider, in 3rd International Colloquium on Theoretical Aspects of Computing (ICTAC'06), Springer-Verlag LNCS, Tunis, Tunisia. 2006. (PDF) (BiBTeX entry)
[11] Reachability Analysis of Generalized Polygonal Hybrid Systems, Gerardo Schneider, In 23rd Annual ACM Symposium on Applied Computing - Software Verification track (SAC-SV'08), ACM, March 2008.
[12] Algorithmic Analysis of Polygonal Hybrid Systems. Part I: Reachability, Eugene Asarin, Gerardo Schneider, and Sergio Yovine, Theoretical Computer Science, 379(1-2):231-265, 2007.
[13] Algorithmic Analysis of Polygonal Hybrid Systems. Part II: Phase Portrait and Tools, Eugene Asarin, Gordon Pace, Gerardo Schneider, and Sergio Yovine, Theoretical Computer Science, 2007.
[14] Computation and Visualisation of Phase Portraits of Polygonal Hybrid Systems, Gordon Pace and Gerardo Schneider, Tools and Algorithms for the Construction and Analysis of Systems (TACAS'08), Springer-Verlag LNCS, Budapest, Hungary, 2008.

The Toolkit

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 is distributed only in source format. To compile the toolkit, you will require a recent version of the Glasgow Haskell Compiler installed on your machine (and make if you plan to use the packaged Makefile). To use the scripting applications (for Meta-SPDIs and parametrised SPDIs) you will also need Perl installed on your machine.

How to compile:
Edit the Makefile so that the SRC and BIN directories point to the right places. By default the makefile assumes that an environment variable SPEEDI is defined, such that the sources can be found in $SPEEDI/src and the executables will be written to $SPEEDI/bin. Just type in 'make'. You can also compile the tools directly using ghc.

Input syntax:
An SPDI file consists of three separate parts. The first is started by the keyword "Points:" under which (in separate lines) one names and defines the points used using the syntax:
point_name. x_coordinate, y_coordinate
Note that the point name is terminated with a fullstop, and the coordinates are separated by a comma. Points are used to define the vertices of the polygons of the SPDI partion. The second part of the file is started by the keyword "Vectors:" (on a separate line) followed by vectors named and defined in a manner identical to that of points:
vector_name. x_coordinate, y_coordinate
Finally, the last part is started by the keyword "Regions:" and contains the SPDI region polygons using the following syntax:
point_1: point_2: ...: point_n: point_1, left_vector, right_vector
The names of the vertices of the polygon (as named in the points section of the input file) are listed in order separated by a colon. Repeat the first point to close the polygon. Finally, the two differential inclusion vector names are given at the end of the line separated by a comma.
Lines in an SPDI file starting with an asterisk are considered to be comments.
An example SPDI file is given to clarify the syntax.

For the syntax of parametrised SPDI files, run the pspdi2spdi script with no parameters to get a description of the input format.

  • 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.

Contact details
Gordon J. Pace
Department of Computer Science,
Faculty of ICT,
University of Malta,
Msida MSD 06,

Tel: (+356) 2340 2504
Fax: (+356) 2132 0539
E-mail: Gordon.Pace@um.edu.mt
Gerardo Schneider
Department of Informatics,
University of Oslo,
P.O. Box 1080 Blindern,
NO-0316 Oslo,

Tel: (+47) 22 85 29 71
Fax: (+47) 22 85 24 01
E-mail: gerardo@ifi.uio.no