A reachability synthesis procedure for discrete event systems in a temporal logic framework

A temporal logic model is introduced to the modeling and design of discrete event systems. Within such a model, the relationship between the reachability of states and the validity of formulas is given to provide a basis for the composition and synthesis of discrete event systems in a temporal logic framework. The composition of temporal logic models is accomplished by formulating a temporal logic model as a process algebra and defining projection applications within the temporal logic models. Procedures are developed for reachability synthesis and a controller logic model is designed to ensure that the required behavior of the system is met. An example of a system of read-write processes is demonstrated to illustrate the novelty of this approach