Mexitl: Multimedia in Executable Interval Temporal Logic

摘要

This paper explores a formalism for describing a wide class of multimedia document constraints, based on an interval temporal logic. We describe the requirements that arise from the multimedia documents application area, and we illustrate these requirements using several examples. Then we present the temporal logic formalism that we use. This logic extends existing interval temporal logic with a number of new features: actions, framing of actions, past operators, a projection-like operator 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.