Computing behavioural relations, logically

Abstract

This paper develops a model-checking algorithm for a fragment of the modal mu-calculus and shows how it may be applied to the efficient computation of behavioral relations between processes. The algorithm’s complexity is proportional to the product of the size of the process and the size of the formula, and thus improves on the best existing algorithm for such a fixed point logic. The method for computing preorders that the model checker induces is also more efficient than known algorithms.