A temporal logic approach to the analysis and synthesis of discrete-event systems.

Abstract

The analysis and synthesis of discrete event systems (DESs) are addressed in this thesis by a temporal logic approach. This approach provides a temporal logic model and a temporal logic language for the modeling and specification, an algorithm for reachability analysis, and a procedure for the controller design and synthesis of DESs. To handle the probabilistic system where the point probability distributions are known, a temporal logic model is defined and a generalized temporal logic language is formulated to include the certainty operators for specifications and verification. An algorithm is developed for computing the reachability set and constructing the reachability graph. Using a process algebra, the composition and synthesis of processes are investigated through the process homomorphism; and a procedure is proposed for the controller synthesis and configuration. Then the optimization problem of DESs is solved by the $A\sp*$ algorithm via a heuristic search. Based on these results, a software package is developed for the temporal logic evaluation, reasoning and simulating discrete event systems. The software is designed using an object-oriented approach and implemented in Objective-C. The simulation results are reported in terms of the logic evaluation, temporal logic reasoning, and discrete event system simulation. Besides, the examples of applications are also given to convey and motivate the theoretical discussions. The results are compared with related works, particularly, qualitative reasoning, other modeling approaches of DESs, and different temporal logic approaches; and our results are seen more advantageous than them in various aspects.