A framework for real-time discrete event control

The TTM/RTTL framework is presented for modeling, specifying, and analyzing real-time discrete event systems. Timed transition models (TTM’s) are used to represent the processes of the plant and its controller. Real-time temporal logic (RTTL) is the assertion language for specifying plant behavior and verifying that a controller satisfies the specifications. The framework adapts features from the program verification literature which are useful for posing problems of interest to the control engineer like modular synthesis and design.