Formal semantics for interactive music scores: a framework to design, specify properties and execute interactive scenarios

Abstract

Most interactive scenarios are based on informal specifications, so that it is not possible to formally verify properties of such systems. We advocate the need for a general and formal model aiming at ensuring safe executions of interactive multimedia scenarios. Interactive scores (is) is a formalism based on temporal constraints to describe interactive scenarios. We propose new semantics for is based on timed event structures (TES). With such a semantics, we can specify more properties of the system, in particular, properties about execution traces, which are difficult to specify as constraints. We also present an operational semantics of is based on the non-deterministic timed concurrent constraint calculus and we relate such a semantics to the TES semantics. With the operational semantics, we can describe the behaviour of scores whose timed object durations can be arbitrary integer intervals.

Keywords:

• event structures
• ccp
• temporal constraint programming
• interaction
• ntcc
• concurrent constraint programming
• interactive music scores
• concurrency
• synchronization

CR Category Numbers::

• D.1.6
• E.4
• H.5.5
• J.5

The authors are grateful to the reviewers for their comments.

Notes

¹There are algorithms to decide the consistency of an stp more efficient than Floyd–Warshall.

²The agent for asynchrony (*) provided by Ntcc is omitted in this paper for simplicity.

³Operational and denotation semantics are explained in Appendices 7 and 8.

⁴Syntax means that the rule is applied zero or more times sequentially.

⁵Agent ∏ represents a generalized parallel composition of processes.

⁶Knapsack picture is taken from the Wikipedia. http://en.wikipedia.org/wiki/Knapsack_problem

Floyd–Warshall has a time complexity of O(n³), where n is the number of events of the event structures semantics of the score.

We use c, d in this paper to represent constraint stores.