  Metric Temporal Logic can express temporally evolving properties with
time-critical constraints or time-triggered constraints for real-time systems.
This paper extends the Metric Interval Temporal Logic with a distribution
eventuality operator to express time-sensitive missions for a system
interacting with a dynamic, probabilistic environment. This formalism enables
us to describe the probabilistic occurrences of random external events as part
of the task specification and event-triggered temporal constraints for the
intended system's behavior. The main contributions of this paper are two folds:
First, we propose a procedure to translate a specification into a stochastic
timed automaton. Second, we develop an approximate-optimal probabilistic
planning problem for synthesizing the control policy that maximizes the
probability for the planning agent to achieve the task, provided that the
external events satisfy the specification. The planning algorithm employs a
truncation in the clocks for the timed automaton to reduce the planning in a
countably infinite state space to a finite state space with a bounded error
guarantee. We illustrate the method with a robot motion planning example.
