Mexitl : Multimedia in Executable Interval Temporal Logic

Howard Bowman, Helen Cameron, Peter King, Simon Thompson

Formal Methods in Systems Design, Kluwer, vol 22 Issue 1, January 2003, pp 5-38.


This paper explores a formalism for describing a wide class of mul- timedia document constraints, based on an interval temporal logic. We describe the requirements that arise from the multimedia documents ap- plication area, and we illustrate these requirements using several exam- ples. Then we present the temporal logic formalism that we use. This logic extends existing interval temporal logic with a number of new fea- tures: actions, framing of actions, past operators, a projection-like op- erator called filter and a new handling of interval length. The notation is applied to the specification of the examples, and in particular a set of logical manipulations, providing feedback to an author, is presented. A model theory, logic and satisfaction relation are defined for the notation.


multimedia, executable, temporal logic, actions, framing, model theory, satisfaction, authoring

Back to Publications