d/dt

d/dt: A Tool for Reachability Analysis of Continuous and Hybrid Systems

Description: d/dt is a tool for reachability analysis of continuous and hybrid systems with linear differential inclusions.

The tool accepts as input a hybrid automaton where:

• Continuous dynamics are linear possibly with uncertain, bounded inputof the form dx/dt = Ax + u where u is input taking values in a bounded convex polyhedron U.
• All staying conditions ("invariants") and transition guards are defined by convex polyhedra.

The problems d/dt can solve:

• Reachability: Given an initial set F, find all the states reachable by the system from F.
• Safety Verification: Given a set B of bad states, check whether the system can reach B.
• Safety Switching Controller Synthesis: Given a safety property specified as a set S of safe states, synthesize a switching controller so that the controlled system always remains inside the safe set S.

Main features:

• Representation of Sets: Reachable sets are represented by orthogonal polyhedra [4].
• Reachability Technique: The approximation of reachable states is based on numerical integration and polyhedral approximation. The Maximum Principle from optimal control is used to deal with uncertain input in continuous dynamics. See [1, 2, 5, 1-0] for more details on the reachability techniques.
• Safety Verification Algorithm: Using forward reachability analysis, the tool computes an over-approximationof the reachable set and checks whether it intersects with the bad set. The output is a yes/no answer accompanied by a set of bad states that the system has reached, in case the answer is yes.
• Switching Controller Synthesis Algorithm: The tool computes an under-approximation of the maximal invariant set (see 2, 1-0]) and derives from this set the switching control laws that restrict the staying conditions and transition guards of the original hybrid automaton so that the resulting automaton meets the desired safety specification.

VO Integration: No

Active: No

Available Benchmarks: No

Website: http://www-verimag.imag.fr/~tdang/ddt.html

Download: Links can be found on the website homepage.

Documentation: There is documentation on the website homepage including a "getting started" section.

Contact: Thao Dang, Oded Maler

Excerpt and graphic from: http://www-verimag.imag.fr/~tdang/ddt.html