Abstract
In this paper we introduce a general semantic interpretation for propositional quantification in all multi-modal logics based on bisimulations (bisimulation quantification). Bisimulation quantification has previously been considered in the context of isolated modal logics, such as PDL (D’Agostino and Hollenberg, 2000), intuitionistic logic (Pitts, 1992) and logics of knowledge (French 2003). We investigate the properties of bisimulation quantifiers in general modal logics, particularly the expressivity and decidability, and seek to motivate the use of bisimulation quantified modal logics. This paper addresses two important questions: when are bisimulation quantified logics bisimulation invariant; and do bisimulation quantifiers always preserve decidability? We provide a sufficient condition for bisimulation invariance, and give two examples of decidable modal logics which are undecidable when augmented with bisimulation quantifiers. This is part of a program of study to characterize the expressivity and decidability of bisimulation quantified modal logics.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berger, R.: The undecidability of the dominoe problem. Mem. Amer. Math. Soc. 66 (1966)
D’Agostino, G.: Modal logic and non-well-founded set theory: translation, bisimulation, interpolation. PhD thesis, University of Amsterdam (1998)
D’Agostino, G., Hollenberg, M.: Logical questions concerning the mu-calculus: interpolation, Lyndon and Los-Tarski. The Journal of Symbolic Logic 65(1), 310–332 (2000)
Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. MIT Press, Cambridge (1995)
Fine, K.: Propositional quantifiers in modal logic. Theoria 36, 336–346 (1970)
French, T.: Decidability of propositionally quantified logics of knowledge. In: Proc. 16th Australian Joint Conference on Artificial Intelligence (2003)
Gabbay, D., Kurucz, A., Wolter, F., Zakharayashev, M.: Many Dimensional Modal Logics: Theory and Applications. Elsevier, Amsterdam (2003)
Ghilardi, S., Zawadowski, M.: A sheaf representation and duality for finitely presented heyting algebras. Journal of Symbolic Logic 60, 911–939 (1995)
Janin, D., Walukiewicz, I.: Automata for the modal mu-calculus and related results. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 552–562. Springer, Heidelberg (1995)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92, pp. 19–27. Springer, Heidelberg (1980)
Park, D.: Concurrency and automata on infinite sequences. In: Deussen, P. (ed.) GI-TCS 1981. LNCS, vol. 104, pp. 167–183. Springer, Heidelberg (1981)
Pitts, A.: On the interpretation of second-order quantification in first-order intuitionistic propositional logic. Journal of Symbolic Logic 57, 33–52 (1992)
van Benthem, J.: Correspondence theory. Handbook of Philosophical Logic 2, 167–247 (1984)
Visser, A.: Uniform interpolation and layered bisimulation. In: Godel 1996. Lecture Notes Logic, vol. 6, pp. 139–164 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
French, T. (2005). Bisimulation Quantified Logics: Undecidability. In: Sarukkai, S., Sen, S. (eds) FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2005. Lecture Notes in Computer Science, vol 3821. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11590156_32
Download citation
DOI: https://doi.org/10.1007/11590156_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30495-1
Online ISBN: 978-3-540-32419-5
eBook Packages: Computer ScienceComputer Science (R0)