Synthesis of controllers for real-time discrete event systems

A (possibly infinite-state) real-time discrete-event plant is modeled as a timed transition system. The free (uncontrolled) behavior of the plant is usually unsatisfactory in some important respect. A specification (written in real-time temporal logic) of required plant behavior is therefore to be imposed on the plant. The key result is a controller development procedure which shows how to systematically develop control strategies for a class of safety properties. The procedure isolates the unsafe part of the behavior, and gives a set of conditions under which the unsafe behavior can be made safe. If the conditions are satisfied, then the plant is guaranteed to satisfy the required specification. The states of the system are not explicitly represented in the design procedure; instead, predicates and predicate transformers, are used to overcome some of the problems of combinatorial explosion of states in large systems