Ariadne is an in-progress open environment to design algorithms for computing with hybrid automata, that relies on a rigorous computable analysis theory to represent geometric objects, in order to achieve provable approximation bounds along the computations. In this paper we discuss the problem of reachability analysis of hybrid automata to decide safety properties. We describe in details the algorithm used in Ariadne to compute over-approximations of reachable sets. Then we show how it works on a simple example. Finally, we discuss the lower-approximation approach to the reachability problem and how to extend Ariadne to support it.
L. Benvenuti, D. Bresolin, A. Casagrande, P. Collins, A. Ferrari, E. Mazzi, et al. (2008). Reachability computation for hybrid systems with Ariadne. Academic Press, Elsevier [10.3182/20080706-5-KR-1001.01513].
Reachability computation for hybrid systems with Ariadne
BRESOLIN, DAVIDE;
2008
Abstract
Ariadne is an in-progress open environment to design algorithms for computing with hybrid automata, that relies on a rigorous computable analysis theory to represent geometric objects, in order to achieve provable approximation bounds along the computations. In this paper we discuss the problem of reachability analysis of hybrid automata to decide safety properties. We describe in details the algorithm used in Ariadne to compute over-approximations of reachable sets. Then we show how it works on a simple example. Finally, we discuss the lower-approximation approach to the reachability problem and how to extend Ariadne to support it.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
