Bisimulation Invariant Monadic-Second Order Logic in the Finite
We consider bisimulation-invariant monadic second-order logic over various classes of finite transition systems. We present several combinatorial characterisations of when the expressive power of this fragment coincides with that of the modal mu-calculus. Using these characterisations we prove for some simple classes of transition systems that this is indeed the case. In particular, we show that, over the class of all finite transition systems with Cantor-Bendixson rank at most k, bisimulation-invariant MSO coincides with L_mu.
bisimulation
monadic second-order logic
composition method
Theory of computation~Finite Model Theory
117:1-117:13
Regular Paper
Achim
Blumensath
Achim Blumensath
Masaryk University Brno
Work supported by the Czech Science Foundation, grant No. GA17-01035S
Felix
Wolf
Felix Wolf
Technische Universität Darmstadt, Institute TEMF, Graduate School of Excellence Computational Engineering
Work partially supported by the \emph{Excellence Initiative} of the German Federal and State Governments and the Graduate School of Computational Engineering at Technische Universität Darmstadt
10.4230/LIPIcs.ICALP.2018.117
H. Andréka, J. van Benthem, and I. Németi. Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic, 27:217-274, 1998.
J. van Benthem. Modal Correspondence Theory. Ph. D. Thesis, University of Amsterdam, Amsterdam, 1976.
A. Blumensath, T. Colcombet, and C. Löding. Logical Theories and Compatible Operations. In J. Flum, E. Grädel, and T. Wilke, editors, Logic and Automata: History and Perspectives, pages 73-106. Amsterdam University Press, 2007.
F. Carreiro. Fragments of Fixpoint Logics. PhD Thesis, Institute for Logic, Language and Computation, Amsterdam, 2015.
I. Ciardelli and M. Otto. Bisimulation in Inquisitive Modal Logic. In Proc. 16th Conference on Theoretical Aspects of Rationality and Knowledge, erTARK 2017, pages 151-166, 2017.
A. Dawar and D. Janin. On the bisimulation invariant fragment of monadic Σ₁ in the finite. In Proc. of the 24th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science, erFSTTCS 2004, pages 224-236, 2004.
E. Grädel, C. Hirsch, and M. Otto. Back and Forth Between Guarded and Modal Logics. ACM Transactions on Computational Logics, pages 418-463, 2002.
E. Grädel, W. Thomas, and T. Wilke. Automata, Logic, and Infinite Games. erLNCS 2500. Springer-Verlag, 2002.
C. Hirsch. Guarded Logics: Algorithms and Bisimulation. Ph. D. Thesis, erRWTH Aachen, Aachen, 2002.
D. Janin and I. Walukiewicz. On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic. In Proc. of the 7th International Conference on Concurrency Theory, erCONCUR 1996, pages 263-277, 1996.
J. A. Makowsky. Algorithmic aspects of the Feferman-Vaught Theorem. Annals of Pure and Applied Logic, 126:159-213, 2004.
F. Moller and A. Rabinovitch. On the expressive power of CTL*. In Proc. 14th erIEEE Symp. on Logic in Computer Science, erLICS, pages 360-369, 1999.
F. Moller and A. Rabinovitch. Counting on CTL*: on the expressive power of monadic path logic. Information and Computation, 184:147-159, 2003.
D. Perrin and J.-É. Pin. Infinite Words - Automata, Semigroups, Logic and Games. Elsevier, 2004.
E. Rosen. Modal logic over finite structures. Journal of Logic, Language and Information, 6:427-439, 1997.
S. Shelah. The Monadic Second Order Theory of Order. Annals of Mathematics, 102:379-419, 1975.
C. Stirling. Bisimulation and logic. In D. Sangiorgi and J. Rutten, editors, Advanced topics in Bisimulation and Coinduction, pages 172-196. Cambridge University Press, 2011.
Achim Blumensath and Felix Wolf
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode