Relational Abstraction
Relational abstraction transforms a hybrid system by replacing the continuous dynamics in each mode by their summary.

Software Download

A tool for creating relational abstractions of HybridSAL models. The output is an infinite state SAL model that can be analyzed using sal-inf-bmc with its various flags.
Download HybridSal.tgz from here (updated new version on Feb 06, 2015).
Download win32_HybridSal.tgz from here for the Cygwin (windows) version (updated Dec, 2014).
Instructions for installing, examples, documentation, etc. can be found in the directory HybridSal; see the file README to get started.


Preferably see the documentation in the doc/ subdirectory under the directory HybridSal. One version of the documentation is here. Slides describing the HybridSAL relational abstractor can be found here.

HybridSal Examples

See examples in the examples/ subdirectory under the directory HybridSal. HybridSal files have a suffix .hsal.

The directory contains examples used in a submission to CAV 15. The examples are also included in the HybridSal release (.tgz) above.

The directory contains files that can be used to create linear hybrid system models of collision avoidance for multiple vehicles . Documentation and results describing the model and its analysis are forthcoming.

Here is a simple example illustrating relational abstraction. A simple example of a switched hybrid system is the LCR circuit controlled by a switch.
Switch open mode: d V_C/dt = 5 - V_C - V_L, d V_L/dt = -5 + V_C -V_L
Switch closed mode: d V_C/dt = 5 - 3 V_C - V_L, d V_L/dt = -5 + 3 V_C - V_L$
Switch from open to closed mode when Vc in [4.5,5.5]
Switch from closed to open mode when Vc in [1,2]

The relational abstraction of this model can be found in lcr.sal.

Relational Abstraction of Navigation Benchmarks

Benchmarks for verification of hybrid systems can be downloaded from here .

We used some of the navigation benchmarks from the above to test the value of the idea of relational abstractions. The nav.sal contains the relational abstractions of the nav01--nav10 benchmarks, along with the safety properties and auxiliary lemmas, whenever they were needed. Under the assumption that the NAV01-NAV06 examples spend atleast 1/10 second in every mode, we generate a stronger relational abstraction, which can be found in the file navZeno.sal

The relational invariants in nav.sal were generated using redlog/qepcad quantifier elimination (see below) procedure. The is a reduce-redlog script that was used to generate the invariants used in nav.sal. The current version of the tool can automatically generate the relational abstraction for linear hybrid systems (such as nav benchmarks). There is no need for QE tools (below).

Quantifier Elimination Tools

If trying to analyze nonlinear hybrid systems using relational abstraction, you will need to create the relational abstraction using QE tools. Here are some freely available tools that can be used to compute relational abstractions -- they provide quantifier elimination and simplification capabilities.


Related to HybridSal and Relational Abstraction:

Other papers (unrelated to HybridSal)


This material is based upon work supported in part by the National Science Foundation, NASA, and Darpa under various grants. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the funding agencies.
This page is maintained by Ashish Tiwari.
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page