On validity in modelization of musical problems by CCP

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. In particular, we show how the expressiveness of ntcc allows to implement complex interactions among musical processes handling different kinds of partial information. The ntcc calculus integrates two dimensions of soft computing: a horizontal dimension dealing with partial information and a vertical one in which non determinism comes into play. This integration is an improvement over constraint satisfaction and concurrent constraint programming models, allowing a more natural representation of a variety of musical processes. We use the nondeterminism 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 realistic musical problem.