Control-invariance of hybrid systems with forcible events

This paper considers controlled hybrid automata with forcible events. First, we introduce two semantics of the controlled hybrid automata using labeled transition systems. Next, we extend a concept of control-invariance in discrete event systems and show necessary and sufficient conditions for a predicate to be control-invariant. Finally, we show that there always exists the supremal control-invariant subpredicate for any predicate.