Using fairness constraints in process-algebraic verification

Although liveness and fairness have been used for a long time in classical model checking, with process-algebraic methods they have seen far less use. One problem is that it is difficult to combine fairness constraints with the compositionality of process algebra. Here we show how a class of fairness constraints can be applied in a consistent way to processes in the compositional setting. We use only ordinary, but possibly infinite, LTSs as our models of processes. In many cases the infinite LTSs are part of a larger system, which can again be represented as a finite LTS. We show how this finiteness can be recovered, namely, we present an algorithm that checks whether a finite representation exists and, if it does, constructs a finite LTS that is equivalent to the infinite system. Even in the negative case, the system produced by the algorithm is a conservative estimate of the infinite system. Such a finite representation can be placed as a component in further compositional analysis just like any other LTS.