Control of Rate-Bounded Hybrid Systems with Liveness Specifications

In the present paper we examine the control problem for a class of composite hybrid machines (CHMs) that consist of concurrent operation (employing synchronous composition) of elementary hybrid machines (EHMs), that allows both signal sharing and event synchronization. A controller can then be coupled with the plant by means of synchronous composition. We confine our attention to controllers that interact with the system only through event synchronization. We present an initial investigation of synthesis of liveness controllers for hybrid machines. To this end we define open hybrid machines as systems that can interact with the environment through event synchronization and can be therefor be "driven" to their marked configuration by user (controller). Liveness specifications must be associated with timing constraints. We may require that for a specified time limit, every run reach a marked configuration within that time limit. Alternatively, a more relaxed specification may be that, for some (unspecified) global time bound, every run of the system reach a marked configuration within that time bound. Finally, the least restrictive liveness requirement is that every run reach a marked configuration within a finite time limit (but we do not insist on the existence of a global time bound for all runs).