LOCAL MODEL CHECKING FOR INFINITE STATE-SPACES

被引:27
作者
BRADFIELD, J
STIRLING, C
机构
[1] Department of Computer Science, University of Edinburgh, Edinburg, EH9 3JZ, The King's Buildings
关键词
D O I
10.1016/0304-3975(92)90183-G
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
We present a sound and complete tableau proof system for establishing whether a set of elements of an arbitrary transition system model has a property expressed in (a slight extension of) the modal mu-calculus. The proof system, we believe, offers a very general verification method applicable to a wide range of computational systems.
引用
收藏
页码:157 / 174
页数:18
相关论文
共 15 条
[1]  
BRADFIELD J, 1990, LECT NOTES COMPUT SC, V458, P115
[2]  
BRADFIELD JC, 1991, LECT NOTES COMPUT SC, V524, P29, DOI 10.1007/BFb0019967
[3]  
DAM MF, IN PRESS 1992 P CAAP
[4]  
Emerson E. Allen, 1986, LICS, P267
[5]  
Fitting M. C., 1983, SYNTHESE LIB, V169
[6]   SNS CAN BE MODALLY CHARACTERIZED [J].
HUTTEL, H .
THEORETICAL COMPUTER SCIENCE, 1990, 74 (02) :239-248
[7]   RESULTS ON THE PROPOSITIONAL MU-CALCULUS [J].
KOZEN, D .
THEORETICAL COMPUTER SCIENCE, 1983, 27 (03) :333-354
[8]   PROOF SYSTEMS FOR SATISFIABILITY IN HENNESSY-MILNER LOGIC WITH RECURSION [J].
LARSEN, KG .
THEORETICAL COMPUTER SCIENCE, 1990, 72 (2-3) :265-288
[9]  
MANNA Z, 1989, LECT NOTES COMPUT SC, V354, P201, DOI DOI 10.1007/BFB0013024
[10]  
Pratt V. R., 1981, 22nd Annual Symposium on Foundations of Computer Science, P421, DOI 10.1109/SFCS.1981.4