Monadic second order logics as model companions of temporal logics

Abstract:

In this talk I will explain an approach to monadic second order (MSO) logic which I am developing in ongoing joint work with Silvio Ghilardi. We exhibit, for various classes of semantic structures, a close connection between MSO logic and the first order theory of the algebras for well-known propositional temporal logics such as LTL and CTL. This connection is given by the classical notion of "model companions", which I will recall in the talk. Specifically, we have proved so far that MSO logic over infinite words gives the model companion of linear temporal logic [1], and that bisimulation invariant MSO logic over infinite trees gives the model companion of a new extension of computation tree logic with local fairness constraints [2].

Proving these results requires two main ingredients: (i) a complete axiomatization of the temporal logic with respect to the intended semantic structures, for which we use Stone duality and a tableau construction; (ii) a conversion from full MSO logic to the existential fragment of the first order theory of the algebras for the temporal logic, for which we use existing correspondences between MSO logic and automata.

References: 

[1] S. Ghilardi and S. J. v. Gool, "A model-theoretic characterization of monadic second-order logic on infinite words", J. Symbolic Logic, vol. 82, no. 1, 62-76 (2017)

[2] S. Ghilardi and S. J. v. Gool, "Monadic second order logic as the model companion of temporal logic", LICS 2016, 417--426 (2016)