Observability Characterization for H-Systems

Abstract

The observability property as defined in Chap. 6 requires the exact discrete state reconstruction in finite time. In the first part of this chapter, we focus specifically on this particular aspect and define the class of current location observable H-systems, that is H-systems for which the current location, i.e. the current discrete state, can be identified after a finite number of steps, either independently from the continuous evolution, or by using also the continuous evolution. The characterization of current location observability for H-systems requires the notion of critical observability, already introduced for FSMs. Then conditions such that an H-system is observable are given, with some results depending on the linearity of the involved dynamics, and hence specific for the class of LH-systems. Finally, we present an approach for reducing the complexity of the verification process, consisting in finding a system that is “equivalent” to the original one with respect to the property that we want to verify but that is “simpler” to analyze.