School of Computing

Mexitl: Multimedia in Executable Interval Temporal Logic

Howard Bowman, Helen Cameron, Peter King, and Simon Thompson

Technical Report 3-97, Computing Laboratory, University of Kent at Canterbury, May 1997.

Abstract

This paper explores a formalism for describing a wide class of multimedia document constraints, based on an interval temporal logic. We describe the requirements on temporal logic specification that arise from the multimedia documents application area. In particular, we highlight a canonical specification example. Then we present the temporal logic formalism that we use. This 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. A model theory, logic and satisfaction relation are defined for the notation, a specification of the canonical example is presented, and a proof system for the logic is introduced.

Download publication 422 kbytes (PostScript)

Bibtex Record

@techreport{226,
author = {Howard Bowman and Helen Cameron and Peter King and Simon Thompson},
title = {{M}exitl: {M}ultimedia in {E}xecutable {I}nterval {T}emporal {L}ogic},
month = {May},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1997/226},
    institution = {Computing Laboratory, University of Kent at Canterbury},
    number = {3-97},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014