Synthesizing Discrete Controllers from Hybrid Automata — Preliminary Report

Hybrid Systems and AI: Modeling Analysis and Control of Discrete Plus Continuous Systems

Volume

Papers from the 1999 AAAI Spring Symposium

Contents

The task of synthesizing and verifying a specification of a controller for a hybrid system is different from the task of synthesizing an executable controller. Specifications of controllers are very useful for the verification of the closedloop system, but the verification procedure often requires that the system behaves in an ideal way. In, e.g., automata approaches, it is typically required that the initial state is known, and that the actual system under control behaves according to its model. In industrial applications such requirements are unrealistic; an industrial controller can never make assumptions about the initial state, and it must be able to handle desynchronizations, i.e. deviations from the expected effects of control actions. In this paper we present preliminary results on how to synthesize robust discrete controllers from a class of Rectangular Hybrid Automata. The language used for the synthesized controllers is Nils Nilsson’s Teleo-Reactive Trees. We prove that the synthesized controllers handle at least the situations for which the original automata is verified.