State structures for verification and real-time control of hybrid automata

We show that the coarsest information structure needed to model a plant (environment) for verification of safety expressed as the avoidance of unsafe states is too coarse for the synthesis of control. The information structure is formulated as a partition of ℜ₊ ⁿ, which represents the state set of the continuous component of a timed automaton, a special case of a linear hybrid automaton. A feedback controller reads the discrete (a location) and continuous (a point in ℜ₊ⁿ) information and produces an actuation by delaying or forcing the occurrence of certain transitions in the plant to ensure that dangerous states would not be reached. Finer information in the form of temporal successors is crucial for control but is not needed for verification. The challenge of finding the coarsest information structure for optimal control is proposed