A temporal logic for reasoning about timed concurrent constraint programs

摘要

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 behavior of timed concurrent constraint programs.