  This paper presents a transformational approach for model checking two
important classes of metric temporal logic (MTL) properties, namely, bounded
response and minimum separation, for nonhierarchical object-oriented Real-Time
Maude specifications. We prove the correctness of our model checking
algorithms, which terminate under reasonable non-Zeno-ness assumptions when the
reachable state space is finite. These new model checking features have been
integrated into Real-Time Maude, and are used to analyze a network of medical
devices and a 4-way traffic intersection system.
