© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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}, }