A linear-time model-checking algorithm for the alternation-free modal mu-calculus |
| |
Authors: | Rance Cleaveland Bernhard Steffen |
| |
Affiliation: | (1) Department of Computer Science, North Carolina State University, 27695-8206 Raleigh, NC, USA;(2) Lehrstuhl für Informatik II, Rheinisch-Westfälische Technische Hochschule Aachen, D-5100 Aachen, Germany |
| |
Abstract: | We develop a model-checking algorithm for a logic that permits propositions to be defined using 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. |
| |
Keywords: | Formal methods in system analysis automated verification model-checking algorithms |
本文献已被 SpringerLink 等数据库收录! |