GRAPHICAL VERSUS LOGICAL SPECIFICATIONS

被引：32

作者：

BOUDOL, G ^{[1
]}

LARSEN, KG ^{[1
]}

机构：

[1] ALBORG UNIV, DK-9000 AALBORG, DENMARK

来源：

THEORETICAL COMPUTER SCIENCE | 1992年 / 106卷 / 01期

关键词：

D O I：

10.1016/0304-3975(92)90276-L

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper studies the relations between two specification formalisms and verification methods for concurrent systems, namely Larsen-Thomsen's modal transition systems-here called graphical specifications-and Hennessy-Milner Logic. We show that any graphical specification may be expressed by a logical specification having the same models. Conversely, we give a characterization of the formulae that are graphically representable.

引用

页码：3 / 20

页数：18

共 16 条

[1]

ARNOLD A, 1990, LECT NOTES COMPUT SC, V407, P117

[2]

BOUDOL G, 1990, LECT NOTES COMPUT SC, V407, P1

[3]

BOUDOL G, 1988, INRIA870 RES REP

[4]

CLEAVELAND R, 1990, LECT NOTES COMPUT SC, V407, P11

[5]

GODSKESEN J, 1989, TAV8919 ALB U DEP MA

[6] A LOGIC FOR THE DESCRIPTION OF NONDETERMINISTIC PROGRAMS AND THEIR PROPERTIES [J].

GRAF, S ;

SIFAKIS, J .

INFORMATION AND CONTROL, 1986, 68 (1-3) :254-270

[7] ALGEBRAIC LAWS FOR NONDETERMINISM AND CONCURRENCY [J].

HENNESSY, M ;

MILNER, R .

JOURNAL OF THE ACM, 1985, 32 (01) :137-161

[8]

HENNESSY M, 1987, CONCURRENCY NETS, P233

[9]

HUTTEL H, 1989, LECT NOTES COMPUT SC, V363, P163

[10]

HUTTEL H, 1988, 8827 ALB U DEP MATH

← 1 2 →