DUALITY AND THE COMPLETENESS OF THE MODAL MU-CALCULUS

被引：13

作者：

AMBLER, S ^{[1
]}

KWIATKOWSKA, M ^{[1
]}

MEASOR, N ^{[1
]}

机构：

[1] UNIV BIRMINGHAM,SCH COMP SCI,BIRMINGHAM B15 2TT,W MIDLANDS,ENGLAND

来源：

THEORETICAL COMPUTER SCIENCE | 1995年 / 151卷 / 01期

关键词：

D O I：

10.1016/0304-3975(95)00045-X

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We consider the modal mu-calculus due to Kozen, which is a finitary modal logic with least and greatest fixed points of monotone operators. We extend the existing duality between the category of modal algebras with homomorphisms and the category of descriptive modal frames with contractions to the case of having fixed point operators. As a corollary, we obtain completeness results for two proof systems due to Kozen (finitary and infinitary) with respect to certain classes of modal frames. The rules are sound in every model, not only for validity.

引用

页码：3 / 27

页数：25

共 25 条

[1] DOMAIN THEORY IN LOGICAL FORM [J].

ABRAMSKY, S .

ANNALS OF PURE AND APPLIED LOGIC, 1991, 51 (1-2) :1-77

[2] DUALITY BEYOND SOBER SPACES - TOPOLOGICAL-SPACES AND OBSERVATION FRAMES [J].

BONSANGUE, MM ;

JACOBS, B ;

KOK, JN .

THEORETICAL COMPUTER SCIENCE, 1995, 151 (01) :79-124

[3] RESEARCH ON AUTOMATIC VERIFICATION OF FINITE-STATE CONCURRENT SYSTEMS [J].

CLARKE, EM ;

GRUMBERG, O .

ANNUAL REVIEW OF COMPUTER SCIENCE, 1987, 2 :269-290

[4]

FINE K, 1974, THEORIA, V40, P23

[5]

Francez N., 1986, FAIRNESS

[6]

Gentzen G., 1969, COLLECTED PAPERS G G

[7]

GOLDBLATT R. I., 1976, REP MATH LOGIC, V6, P41

[8]

GOLDBLATT RI, 1976, REPORTS MATH LOGIC, V7, P21

[9]

Halmos P., 1962, ALGEBRAIC LOGIC

[10]

HUGHES GE, 1984, COMPANION MODAL LOGI

← 1 2 3 →