Proving Musical Properties using a temporal Concurrent Constraint Calculus

We show how the ntcc calculus, a model of temporal concurrent constraint programming with the capability of modeling asynchronous and non-deterministic timed behavior, can be used for modeling real musical processes. We use the non-determinism facility of ntcc to build weaker representations of musical processes that greatly simplifies the formal expression and analysis of its properties. We argue that this modeling strategy provides a "runnable specification" for music problems that eases the task of formally reasoning about them. We show how the linear temporal logic associated with ntcc gives a very expressive setting for formally proving the existence of interesting musical properties of a process. We give examples of musical specifications in ntcc and use the linear temporal logic for proving properties of a real musical problem.