Abstract
One of van Benthem’s seminal results is the Bisimulation Theorem characterizing modal logic as the bisimulation-invariant fragment of first-order logic. Janin and Walukiewicz extended this theorem to include fixpoint operators, showing that the modal \({\mu }\)-calculus \({\mu }\)ML is the bisimulation-invariant fragment of monadic second-order logic MSO. Their proof uses parity automata that operate on Kripke models, and feature a transition map defined in terms of certain fragments of monadic first-order logic. In this paper we decompose their proof in three parts: (1) two automata-theoretic characterizations, of MSO and \(\mu \)ML respectively, (2) a simple model-theoretic characterization of the identity-free fragment of monadic first-order logic, and (3) an automata-theoretic result, stating that (a strong version of) the second result somehow propagates to the level of full fixpoint logics. Our main contribution shows that the third result is an instance of a more general phenomenon that is essentially coalgebraic in nature. We prove that if one set \(\varLambda \) of predicate liftings (or modalities) for a certain set functor \(T\) uniformly corresponds to the \(T\)-natural fragment of another such set \(\varLambda ^{\prime }\), then the fixpoint logic associated with \(\varLambda \) is the bisimulation-invariant logic of the fixpoint logic associated with \(\varLambda ^{\prime }\).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
Here the tacit understanding is that the variable \(v\) is interpreted as the root of the tree.
References
Andréka H, van Benthem J, Németi I (1998) Modal languages and bounded fragments of predicate logic. J Philos Log 27:217–274
van Benthem J (1976) Modal correspondence theory. PhD thesis, Mathematisch Instituut & Instituut voor Grondslagenonderzoek, University of Amsterdam
van Benthem J (1984) Correspondence theory. In: Gabbay DM, Guenthner F (eds) Handbook of philosophical logic, vol 2. Reidel, Dordrecht, pp 167–247
ten Cate B, Gabelaia D, Sustretov D (2009) Modal languages for topology: expressivity and definability. Ann Pure App Log 159(1–2):146–170
Cîrstea C, Kurz A, Pattinson D, Schröder L, Venema Y (2011) Modal logics are coalgebraic. Comput J 54:524–538
Cîrstea C, Kupke C, Pattinson D (2009) EXPTIME tableaux for the coalgebraic \(\mu \)-calculus. In: Grädel E, Kahle R (eds) Computer science logic 2009. Lecture notes in computer science, vol 5771. Springer, New York, pp 179–193
D’Agostino G, Hollenberg M (2000) Logical questions concerning the \(\mu \)-calculus. J Symbol Log 65:310–332
Dawar A, Otto M (2009) Modal characterisation theorems over special classes of frames. Ann Pure Appl Log 161:1–42
Fontaine G, and Venema Y (2010) Some model theory for the modal mu-calculus: syntactic characterizations of semantic properties (Manuscript, submitted)
Fontaine G, Leal R, Venema Y (2010) Automata for coalgebras: an approach using predicate liftings. In: Abramsky s et al. (eds) Proceedings of ICALP 2010, part II. LNCS, vol 6199. Springer, New York
Grädel E, Hirsch C, Otto M (2002) Back and forth between guarded and modal logics. ACM Trans Comput Log 3:418–463
Grädel E, Thomas W, Wilke T (eds) (2002) Automata, logic, and infinite games. LNCS, vol 2500. Springer, New York
Janin D, Walukiewicz I (1995) Automata for the modal \(\mu \)-calculus and related results. In: Proceedings of the twentieth international symposium on mathematical foundations of computer science, MFCS’95. LNCS, vol 969. Springer, New York, pp 552–562
Janin D, Walukiewicz I (1996) On the expressive completeness of the propositional \(\mu \)-calculus w.r.t. monadic second-order logic. In: Proceedings CONCUR ’96
Litak T, Pattinson D, Sano K, Schröder L (2012) Coalgebraic predicate logic. In: Czumaj A et al. (eds) ICALP 2012. Lecture notes in computer science, vol 7392. Springer, New York, pp 299–311
Moss L (1999) Coalgebraic logic. Ann Pure Appl Log 96:277–317 (Erratum published Ann P Appl Log 99:241–259)
Otto M (2011) Model theoretic methods for fragments of fo and special classes of (finite) structures. In: Esparza J, Michaux C, Steinhorn C (eds) Finite and algorithmic model theory. LMS Lecture notes series, vol 379. Cambridge University Press, Cambridge
Pattinson D (2003) Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theor Comput Sci 309(1–3):177–193
Rosen E (1997) Modal logic over finite structures. J Log Lang Inf 6:427–439
Rutten J (2000) Universal coalgebra: a theory of systems. Theor Comput Sci 249:3–80
Venema Y (2006) Algebras and coalgebras. In: van Benthem J, Blackburn P, Wolter F (eds) Handbook of modal logic. Elsevier, Amsterdam, pp 331–426
Venema Y (2006) Automata and fixed point logic: a coalgebraic perspective. Inf Comput 204:637–678
Walukiewicz I (2002) Monadic second-order logic on tree-like structures. Theor Comput Sc 275:311–346
Acknowledgments
The research of this author has been made possible by VICI grant 639.073.501 of the Netherlands Organization for Scientific Research (NWO). Furthermore, the author is grateful to Facundo Carreiro for many comments on an earlier version of the paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Venema, Y. (2014). Expressiveness Modulo Bisimilarity: A Coalgebraic Perspective. In: Baltag, A., Smets, S. (eds) Johan van Benthem on Logic and Information Dynamics. Outstanding Contributions to Logic, vol 5. Springer, Cham. https://doi.org/10.1007/978-3-319-06025-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-06025-5_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06024-8
Online ISBN: 978-3-319-06025-5
eBook Packages: Humanities, Social Sciences and LawPhilosophy and Religion (R0)