作者
Ranee Cleaveland, Marion Klein, Bernhard Steffen
发表日期
1993
研讨会论文
Computer Aided Verification: Fourth International Workshop, CAV'92 Montreal, Canada, June 29–July 1, 1992 Proceedings 4
页码范围
410-422
出版商
Springer Berlin Heidelberg
简介
In this paper, we develop an algorithm for model checking that handles the full modal mucalculus including alternating fixpoints. Our algorithm has a better worst-case complexity than the best known algorithm for this logic while performing just as well on certain sublogics as other specialized algorithms. Important for the efficiency is an alternative characterisation of formulas in terms of equational systems, which enables the sharing and reuse of intermediate results.
引用总数
1992199319941995199619971998199920002001200220032004200520062007200820092010201120122013201420152016201720182019202020212022202320241710912877813121166796333244452332421
学术搜索中的文章
R Cleaveland, M Klein, B Steffen - … Aided Verification: Fourth International Workshop, CAV …, 1993