Modeling Timed Systems with Temporal Concurrent Constraint Programming

In this talk I shall describe a temporal concurrent constraint programming process calculus, called ntcc, for modeling discrete  timed systems.  A modal logic for specifying (temporal) properties of  ntcc processes will be defined together with a (relatively complete) inference system for proving that a process satisfies a formula in  the logic. I shall also define behavioral notions that reflect the infinite reactive interactions between processes and their environment  as well as internal interactions between individual processes. The notions are proven to be decidable for a substantial fragment of the calculus. Furthermore, some examples will be shown to illustrate the expressiveness of the calculus.

The talk will not presuppose any knowledge of concurrent constraint programming.