When Are Prime Formulae Characteristic?

被引：3

作者：

Aceto, L. ^{[1
]}

Della Monica, D. ^{[1
]}

Fabregas, I. ^{[1
]}

Ingolfsdottir, A. ^{[1
]}

机构：

[1] Reykjavik Univ, Sch Comp Sci, ICE TCS, Reykjavik, Iceland

来源：

MATHEMATICAL FOUNDATIONS OF COMPUTER SCIENCE 2015, PT I | 2015年 / 9234卷

关键词：

BISIMULATION;

D O I：

10.1007/978-3-662-48057-1_6

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

In the setting of the modal logic that characterizes modal refinement over modal transition systems, Boudol and Larsen showed that the formulae for which model checking can be reduced to preorder checking, that is, the characteristic formulae, are exactly the consistent and prime ones. This paper presents general, sufficient conditions guaranteeing that characteristic formulae are exactly the consistent and prime ones. It is shown that the given conditions apply to the logics characterizing all the semantics in van Glabbeek's branching-time spectrum.

引用

页码：76 / 88

页数：13

共 13 条

[1] Aceto L., ARE PRIME FORMULAE C
[2] Aceto L., 2007, REACTIVE SYSTEMS MOD
[3] Graphical representation of covariant-contravariant modal formulae
Aceto, Luca
Ingolfsdottir, Anna
Fabregas, Ignacio
Escrig, David de Frutos
Palomino, Miguel
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2011, (64): : 1 - 15
[4] BISIMULATION CANT BE TRACED
BLOOM, B
ISTRAIL, SN
MEYER, AR
[J]. JOURNAL OF THE ASSOCIATION FOR COMPUTING MACHINERY, 1995, 42 (01): : 232 - 268
[5] GRAPHICAL VERSUS LOGICAL SPECIFICATIONS
BOUDOL, G
LARSEN, KG
[J]. THEORETICAL COMPUTER SCIENCE, 1992, 106 (01) : 3 - 20
[6] Clarke EM, 1999, MODEL CHECKING, P1
[7] CLEAVELAND R, 1991, LECT NOTES COMPUT SC, V510, P127
[8] de Frutos-Escrig D., 2013, LOG METH COMPUT SCI, V9, P1
[9] A MODAL CHARACTERIZATION OF OBSERVATIONAL CONGRUENCE ON FINITE TERMS OF CCS
GRAF, S
SIFAKIS, J
[J]. INFORMATION AND CONTROL, 1986, 68 (1-3): : 125 - 145
[10] FORMAL VERIFICATION OF PARALLEL PROGRAMS
KELLER, RM
[J]. COMMUNICATIONS OF THE ACM, 1976, 19 (07) : 371 - 384

← 1 2 →