Abstract
We investigate the expressive power of existential monadic second-order logic (monadic Σ1) on finite transition systems. In particular, we look at its power to express properties that are invariant under forms of bisimulation and compare these to properties expressible in corresponding fixed-point modal calculi. We show that on finite unary transition systems the bisimulation invariant fragment of monadic Σ1 is equivalent to bisimulation-invariant monadic second order logic itself or, equivalently, the mu-calculus. These results contrast with the situation on infinite structures. Although we show that these results do not extend directly to the case of arbitrary finite transition systems, we are still able to show that the situation there contrasts sharply with the case of arbitrary structures. In particular, we establish a partial expressiveness result by means of tree-like tiling systems that does not hold on infinite structures.
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.
Similar content being viewed by others
References
Ajtai, M., Fagin, R.: Reachability is harder for directed rather than undirected finite graphs. Journal of Symbolic Logic 55, 113–150 (1990)
Bradfield, J.: The modal mu-calculus alternation hierarchy is strict. Theoretical Computer Science 195, 133–153 (1998)
Ebbinghaus, H.-D., Flum, J.: Finite Model Theory, 2nd edn. Springer, Heidelberg (1999)
Janin, D., Lenzi, G.: On the logical definability of topologically closed recognizable languages of infinite trees. Computing and Informatics 21, 185–203 (2002)
Janin, D., Walukiewicz, I.: On the expressive completeness of the modal mu-calculus with respect to monadic second order logic. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 263–277. Springer, Heidelberg (1996)
Makowski, J.A., Ravve, E.: Incremental model checking for decomposable strutures. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 540–551. Springer, Heidelberg (1995)
Otto, M.: Modal and guarded characterisation theorems over finite transition systems. In: Proc. of the 17th IEEE Symp. on Logic in Computer Science (LICS), pp. 371–380 (2002)
Rosen, E.: Modal logic over finite structures. Journal of Logic, Language and Information 6, 427–439 (1997)
Schwentick, T., Barthelmann, K.: Local normal forms for first-order logic with applications to games and automata. Discrete Mathematics and Theoretical Computer Science 3, 109–124 (1999)
Thomas, W.: Automata theory on trees and partial orders. In: Bidoit, M., Dauchet, M. (eds.) CAAP 1997, FASE 1997, and TAPSOFT 1997. LNCS, vol. 1214, pp. 20–38. Springer, Heidelberg (1997)
van Benthem, J.: Modal Logic and Classical Logic. Bibliopolis (1983)
Walukiewicz, I.: Monadic second order logic on tree-like structures. In: STACS 1996. LNCS, vol. 1046. Springer, Heidelberg (1996); Full version in Information and Computation 164, 234–263 (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dawar, A., Janin, D. (2004). On the Bisimulation Invariant Fragment of Monadic Σ1 in the Finite. In: Lodaya, K., Mahajan, M. (eds) FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2004. Lecture Notes in Computer Science, vol 3328. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30538-5_19
Download citation
DOI: https://doi.org/10.1007/978-3-540-30538-5_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24058-7
Online ISBN: 978-3-540-30538-5
eBook Packages: Computer ScienceComputer Science (R0)