• AIB 2016-02: Comparative Evaluation and Improvement of Computational Ap

    From Jera Hensel@21:1/5 to All on Sun Apr 3 12:36:22 2016
    The following technical report is available from http://aib.informatik.rwth-aachen.de:

    Comparative Evaluation and Improvement of Computational Approaches to Reachability Analysis of Linear Hybrid Systems
    Ibtissem Ben Makhlouf
    AIB 2016-02

    This thesis addresses the problem of reachability analysis with the
    focus on linear hybrid systems. Hybrid systems are a mixture of
    continuous and discrete behaviors. The Hybrid automaton consisting of a
    graph, in which the locations describe the continuous and the
    transitions the discrete behavior, represents the best formal model for
    such kind of systems. It provides a formalism integrating differential equations and logic expressions in a same framework, thus opening new
    horizons in research and development of new methods and novel
    algorithms. Despite recent progress made in this field in the last
    years, actual verification methods and available tools have exhibited
    their shortcomings.

    We started this work with the assessment of some verification tools
    using a suite of benchmarks conceived specially for this task. The
    benchmarks possess particular characteristics for testing of efficiency, applicability, scalability, capability and performances of these tools.

    We offer a theoretical overview of existing methods for computing an overapproximation of reachable sets for linear time invariant hybrid
    systems. This covers approaches for overapproximating reachable sets of
    the continuous dynamics with and without invariants as well as methods
    for solving the problem of guard intersection at transitions. We
    furthermore propose new overapproximation techniques for treating the continuous part as well as the discrete part of the hybrid automaton. We suggest scalable, modular implementations of these diverse methods
    allowing thereby possible combinations between them first using support functions and then with zonotopes. The implementations include different approaches for handling invariants, guards and transitions for the above-mentioned set representations. Two toolboxes are the results of
    this implementation effort. Both tools integrate the methods described
    above. They offer a GUI and allow for a user-configurable reachability analysis. We use both tools to carry out a performance comparison of
    different methods. We note thereby that there is a correlation between
    these performances and the complexity of the tested example. However, we
    note during this survey using the proposed benchmark suite that the
    difference in the performance with regards to the tightness of the over-approximation and the computation time is not so crucial for low dimensional systems.

    We propose a networked platoon of vehicles to demonstrate different
    context where reachability analysis can be useful. We first perform a reachability analysis to determine unsafe gaps between the vehicles
    which are controlled using LMI-formalism. Reachability analysis can be
    helpful for control design. The choice between controllers on the basis
    of reachability results has led to controller ensuring the best
    compromise between safe and small gaps when applying H2 or H<UTF16-221E> control
    design techniques. Reachability can also be used to determine
    time-critical conditions. As demonstration, we opt for a platoon
    approaching an intersection.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)