Taming Heterogeneity and Complexity of Embedded Control

Observability of Hybrid Automata by Abstraction

Alessandro D'Innocenzo, Maria Domenica Di Benedetto and Stefano Di Gennaro

Department of Electrical and Information Engineering and Center of Excellence DEWS, University of L'Aquila, Italy adinnoce, dibenede, [e-mail]

ABSTRACT. In this paper, we deal with the observability problem of a class of Hybrid Systems whose output is a timed string on a finite alphabet. We determine under which conditions it is always possible to immediately detect, using the observed output, when the system enters a given discrete state. We illustrate how to construct a Timed Automaton that is an abstraction of the given Hybrid System, and that preserves its observability properties. Moreover, we propose a verification algorithm with polynomial complexity for checking the observability of the Timed Automaton, and a constructive procedure for an observer of the discrete state.

KEYWORDS: Hybrid Systems, Timed Automata, Observability

1. Introduction

The issue of observability is an interesting open problem in the context of Hybrid Systems, whose significance is widely recognized in safety critical applications (e.g. Air Traffic Management) or failure detection applications (e.g. software monitoring and telecommunications). Observability of Hybrid Systems was extensively studied in the literature [BAB 05, De 03, OIS 03, VID 03], while observer design was considered e.g. in [BAL 02]. In this work, we provide a definition of observability of a ...