A temporal logic approach to discrete event control

This paper presents a temporal logic formulation of discrete event control which forms a new theoretical basis for control analysis and synthesis of a class of discrete event systems (DES). Specifically, the new basic notions of controllability, control invariance and Σ_u-invariance are characterized for a safety temporal logic formula, and the necessary and sufficient condition for the existence of its supervisor is established. The existing result based on the predicate approach is shown to be generalized under our formulation. A control synthesis procedure is given for a class of DES based on a specialized safety formula, known as the forbidden state specification. Two simple examples illustrate the proposed axiomatic approach