Back and forth between guarded and modal logics

Author

Gradel, Erich ; Hirsch, Colin ; Otto, Martin

Author_Institution

Math. Grundlagen der Inf., Tech. Hochschule Aachen, Germany

fYear

2000

fDate

2000

Firstpage

217

Lastpage

228

Abstract

Guarded fixed point logic μGF extends the guarded fragment by means of least and greatest fixed points, and thus plays the same role within the domain of guarded logics as the modal μ-calculus plays within the modal domain. We provide a semantic characterisation of μGF within an appropriate fragment of second-order logic, in terms of invariance under guarded bisimulation. The corresponding characterisation of the modal μ-calculus, due to D. Janin and I. Walukiewicz (1999), is lifted from the modal to the guarded domain by means of model theoretic translations. At the methodological level, these translations make the intuitive analogy between modal and guarded logics available as a tool in the analysis of the guarded domain

Keywords

bisimulation equivalence; calculus; formal logic; theorem proving; μGF; fixed points; guarded bisimulation; guarded fixed point logic; guarded fragment; intuitive analogy; invariance; modal μ-calculus; modal domain; modal logics; model theoretic translations; second-order logic; semantic characterisation; Automata; Calculus; Context modeling; Heart; Logic;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on

Conference_Location

Santa Barbara, CA

ISSN

1043-6871

Print_ISBN

0-7695-0725-5

Type

conf

DOI

10.1109/LICS.2000.855771

Filename

855771