At this moment, there lacks a specification language for distributed real-time system properties involving states and events. There also lacks a language for fairness assumptions in dense-time systems. We have defined a new temporal logic, TECTL f , for the flexible specification of distributed real-time systems with constraints involving events, states, and fairness assumptions. Then we have also designed algorithms for model-checking TECTL f formulas. Finally, we have endeavored to implement and experiment the ideas in our tool, Red 5.1, and shown that the ideas could be used in practice.