Fairness Assumptions for Csp in a Temporal Logic Framework

摘要

Six fairness assumptions for the repetitive construct ...(square)b sub l, c sub l yields S sub l(square)... in a subset of communicating sequential processes (CSP) are given and classified with respect to the programs they cause to terminate. A total correctness proof system for the subset of CSP is given, incorporating the different fairness assumptions.