Theorem of abstraction for equivalent controllers in hybrid systems

In the analysis and synthesis of controllers for hybrid systems, it is often required to verify whether two controllers for a given hybrid plant are equivalent. This is not easy to do because one needs to verify that the two controlled hybrid systems generate the same sequence of discrete events and the same trajectory for continuous variables for the given initial conditions. In this paper, we prove that under certain conditions, the verification of equivalence can be done at the abstract level of discrete event systems. More precisely, two controllers are equivalent if and only if the languages (that is, the sets of all possible sequences of discrete transitions) generated by two controlled systems are the same. This theorem of abstraction implies that many control problems of hybrid systems can be studied at the abstract level of discrete event systems. Therefore, it can be used in the control synthesis for decentralized controllers and partial observation controllers because techniques developed for discrete event systems can now be applied to hybrid systems.