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 Aug 28, 2012).
Instructions for installing, examples, documentation, etc. can be found in the directory HybridSal. Latest version of the documentation is here. Slides describing the HybridSAL relational abstractor can be found here.

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.

Quantifier Elimination Tools

These are some freely available tools that can be used to compute relational abstractions by providing quantifier elimination and simplification capabilities.

Publications

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.

People Involved

Sriram Sankaranarayanan
Ashish Tiwari
Aditya Zutshi

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