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.
CITATION STYLE
Cleaveland, R., & Steffen, B. (1992). A linear-time model-checking algorithm for the alternation-free modal mu-calculus. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 575 LNCS, pp. 48–58). Springer Verlag. https://doi.org/10.1007/3-540-55179-4_6
Mendeley helps you to discover research relevant for your work.