The production of efficient and adequate temporal reasoning methods for concurrent systems is a long range goal of this project. A branching time model with intervals as the underlying unit of time will be used to represent constructs from concurrent programming. In particular, the following tasks shall be undertaken: O Establish the correctness of twenty-four atomic relations between intervals in branching time and the table of their compositions. O Create a formal interpretation of executions of concurrent programs in terms of the model. O Determine the expression in the model of the important concurrency relationships such as mutual exclusion, deadlock freedom, and fairness.
