作者
Rance Cleaveland, Bernhard Steffen
发表日期
1993/4
期刊
Formal methods in system design
卷号
2
页码范围
121-147
出版商
Kluwer Academic Publishers
简介
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.
引用总数
学术搜索中的文章
R Cleaveland, B Steffen - Formal methods in system design, 1993
R Cleaveland, B Steffen - … Aided Verification: 3rd International Workshop, CAV'91 …, 1992