This paper presents on-going work using a formal approach for the design of Interactive Multimedia Documents (IMDs) based on the RT-LOTOS formal description technique. This work addresses more particularly the scheduling and presentation of IMDs based on a simple scheduling graph, called TLA, which is automatically derived from the document formal specification. For this purpose we present some scheduling algorithms and some implementation aspects of the resultant TLA Player. Further on, some contributions are presented concerning the optimization of pre-fetching techniques implemented in the TLA Player. At last, we present the results of some tests performed to validate the behavior of the player.