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

共 50 条

[31] EQUATIONAL MU-CALCULUS
NIWINSKI, D
LECTURE NOTES IN COMPUTER SCIENCE, 1985, 208 : 167 - 176
[32] Lukasiewicz mu-calculus
Mio, Matteo
Simpson, Alex
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (126): : 87 - 104
[33] The Horn mu-calculus
Charatonik, W
McAllester, D
Niwinski, D
Podelski, A
Walukiewicz, I
THIRTEENTH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1998, : 58 - 69
[34] Uniform Interpolation from Cyclic Proofs: The Case of Modal Mu-Calculus
Afshari, Bahareh
Leigh, Graham E.
Turata, Guillermo Menendez
AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2021, 2021, 12842 : 335 - 353
[35] Model checking the full modal mu-calculus for infinite sequential processes
Burkart, O
Steffen, B
THEORETICAL COMPUTER SCIENCE, 1999, 221 (1-2) : 251 - 270
[36] COMPLEXITY OF MODEL CHECKING RECURSION SCHEMES FOR FRAGMENTS OF THE MODAL MU-CALCULUS
Kobayashi, Naoki
Ong, C-H Luke
LOGICAL METHODS IN COMPUTER SCIENCE, 2011, 7 (04) : 1 - 23
[37] Modal Mu-calculus Extension with Description of Autonomy and Its Algebraic Structure
Yamasaki, Susumu
Sasakura, Mariko
PROCEEDINGS OF THE 5TH INTERNATIONAL CONFERENCE ON COMPLEXITY, FUTURE INFORMATION SYSTEMS AND RISK (COMPLEXIS), 2020, : 63 - 71
[38] Continuous Fragment of the mu-Calculus
Fontaine, Gaelle
COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2008, 5213 : 139 - 153
[39] Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus
Kobayashi, Naoki
Ong, C. -H. Luke
AUTOMATA, LANGUAGES AND PROGRAMMING, PT II, PROCEEDINGS, 2009, 5556 : 223 - +
[40] Model checking the full modal mu-calculus for infinite sequential processes
Burkart, O
Steffen, B
AUTOMATA, LANGUAGES AND PROGRAMMING, 1997, 1256 : 419 - 429

← 1 2 3 4 5 →