Relational Abstraction

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.

Documentation

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

Publications

Related to HybridSal and Relational Abstraction:

A. Tiwari. Time-Aware Abstractions in HybridSal. In CAV 2015.
Sergio Mover, Alessandro Cimatti, Ashish Tiwari and Stefano Tonetta, "Time-aware relational abstraction for Hybrid systems", In EMSOFT 2013.
Sriram Sankaranarayanan and Ashish Tiwari, Relational Abstractions for Continuous and Hybrid Systems. (Full version of a submitted paper with the same title)
Ashish Tiwari, HybridSal Relational Abstracter.
Additional documentation can be found in the doc/ subdirectory of the HybridSal tool.

Other papers (unrelated to HybridSal)

A. Tiwari. "Attacking a feedback controller". In NSV 2015.
With Martin Schaef. Severity levels of inconsistent code. To appear. ATVA 2015.
With Adria Gascon and Manfred Schmidt-Schauss. Two-restricted one context unification is in polynomial time. To appear. CSL 2015.
With Adria Gascon and Manfred Schmidt-Schauss. One context unification problems solvable in polynomial time. In LICS 2015.

Acknowledgments

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