|
Logic & Semantics |
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.