Abstract:
We propose an extension of Timed Default Concurrent Constraint language designed by Saraswat and Gupta. Our proposal is to replace Gentzen constraint system by a mixed constraint system with boolean formulas and linear constraints over rationals. We then propose using model checking like proposed in CLP by Delzanno and Podelski, to verify synchronous programs in Timed Default CC. This allows to deal with properties of numerical variables.

Slides (.pdf)