next up previous
Next: The Plant Model Up: Timed Transition Models Previous: Timed Transition Models

Introduction

Timed Transition Models (TTM's) are an extension of state machines. They were introduced by Ostroff [14] in describing a plant model P for real time DES's. In this framework specifications are described using Real Time Temporal Logic (RTTL). With RTTL, one can describe the system behavior that is to be imposed on the plant in terms of the variables of the TTM's, and one can also verify that the correct behavior is obtained. The specifications used in this procedure, however, are restricted to a class of safety properties. In order to develop the controller C, the ``unsafe'' states are identified and a set of sufficient conditions are obtained under which the unsafe behavior can be made safe. The procedure then ``backtracks'' one step to the states that bring the system to each of the unsafe states. If possible, the procedure adopts a controlling strategy (for example by changing the ``enabling'' functions of the unsafe transitions), and the plant is guaranteed to satisfy the safety requirements. If not, then the algorithm backtracks one more step, and the above procedure is repeated. One drawback of this method is that the controlling strategies developed, though sufficient, may not be necessary for the plant to satisfy the safety requirements (e.g. if the unsafe states are unreachable). That is, the procedure may be too conservative. Below we present a summary of Ostroff's work in [14].



Luz E. Pinzon
Wed Oct 15 18:10:49 EDT 1997