ntccMC: A bounded-time model checker for ntcc

A disadvantage of concurrent constraint programming (ccp) calculi isthat it is difficult to exploit its declarative point of view because of the lackof automated verification tools available. This limits the applicability of theverification techniques to small problems. As an example, a model checkerfor a non-deterministic timed concurrent constaint (ntcc) will be useful notonly for music systems, but for many other fields on which ccp has beenproven successful (e.g., system biology and security systems). We claimfor the urgent need of a model checker for ntcc. First, because ntcc hasbeen widely used to model reactive system and verify properties about them,but the verification had to be done by hand. Second, because there are notmany frameworks to formally model and verify music interaction systemsand ntcc has been proved to be successful in that field. In this paper wepropose a model checker for ntcc.