A temporal logic for reasoning about timed concurrent constraint programs

Abstract

A temporal logic is presented for reasoning about the correctness of timed concurrent constraint programs. The logic is based on epistemic modalities which express either what a process knows at a certain time or what a process believes about the results of the other processes. In terms of these epistemic modalities of knowledge and belief a compositional axiomatization is given of the reactive behaviour of timed concurrent constraint programs.