Balluchi, Andrea (PARADES), Casagrande, Alberto (Univ. of Udine), Collins, Pieter (Centrum voor Wiskunde en Informatica), Ferrari, Alberto (PARADES), Villa, Tiziano (Univ. of Udine), Sangiovanni-Vincentelli, Alberto L. (Univ. of California)

Ariadne: A Framework for Reachability Analysis of Hybrid Automata

Scheduled for presentation during the Regular Session "Hybrid Systems I" (WeA05), Wednesday, July 26, 2006, 10:25−10:50, Room F

17th International Symposium on Mathematical Theory of Networks and Systems, July 24-28, 2006, Kyoto, Japan

This information is tentative and subject to change. Compiled on April 26, 2024

Abstract

In this paper we introduce the problem of reachability analysis of hybrid automata to decide safety properties. Then we describe Ariadne, an in-progress open environment to design algorithms for computing with hybrid automata. We show that Ariadne relies on a rigorous computable analysis theory to represent geometric objects, in order to achieve provable approximation bounds along the computations. The proposed tool differs from existing ones because it relies on a sound theoretical basis for the semantics of operators in continuous space and time, making available exact and approximate, but error-bounded operations on geometric points and sets. Currently the geometry module is substantially completed, and work is in progress on the evaluation module. As a first application, we will use Ariadne to compute the reachable sets of a challenging collection of benchmarks whose safety properties have practical interest.