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.
Note: A journal version subsumes this paper.
We develop a model-checking algorithm for a logic that permits propositions to be defined with greatest and least fixed points of mutually recursive systems of equations. This logic is as expressive as the alternation-free fragment of the modal mu-calculus identified by Emerson and Lei, and it may therefore be used to encode a number of temporal logics and behavioral preorders. Our algorithm determines whether a process satisfies a formula in time proportional to the product of the sizes of the process and the formula; this improves on the best known algorithm for similar fixed-point logics.
Note: A journal version subsumes this paper.
This paper develops a framework for generating testing preorders that relate processes on the basis of their timing behavior as well as their degree of relative nondeterminism. The framework is then applied to two different scenarios. In the first, relations are constructed that relate processes on the basis of all timing considerations. In the second, relations are constructed that relate processes on the basis of their relative speeds. In both cases, alternative denotational characterizations of the resulting preorders are presented, and examples are givem to illustrate the utility of the approach.
| Go to Rance Cleaveland's publication home page. |
Last modified: August 13, 1998
Rance Cleaveland