  In this paper we propose a language for conveniently defining a wide range of
execution strategies for real-time rewrite theories, and provide
Maude-strategy-implemented versions of most Real-Time Maude analysis methods,
albeit with user-defined discrete and timed strategies. We also identify a new
time sampling strategy that should provide both efficient and exhaustive
analysis for many distributed real-time systems. We exemplify the use of our
language and its analyses on a simple round trip time protocol, and compare the
performance of standard Maude search with our strategy-implemented reachability
analyses on the CASH scheduling algorithm benchmark.
