A logic for real-time discrete event processes

Temporal logic can be used to design controllers for real-time discrete event systems. The underlying plant dynamics is most economically described by a state transition structure with time bounds on the transitions. Temporal logic can then be used to specify the problem to be solved and help in the derivation and verification of a suitable controller. The author discusses the nature of real-time discrete event processes, examines the software verification literature, gives a brief overview of the model and logic framework, and provides a small example of controller design.<>