Analysis and synthesis procedures of discrete event systems in a temporal logic framework

A model, based on event structures, a set of temporal logic formulas, an initial state, and a labeling function, for the characterization of discrete event systems (DES) is proposed and used for the investigation of system properties such as verification and reachability. For the synthesis procedure, as applied to DES, a composition rule of 2 systems is developed, and a controller design procedure is introduced. An example of a computer file system is used to illustrate this approach