Monadic second order logic as the model companion of temporal logic

TL;DR

This paper establishes a novel model-theoretic framework linking monadic second order logic and a new temporal logic called fair CTL, using bisimulation invariance and automata encoding.

Contribution

It introduces fair CTL as a new temporal logic with a model companion derived from bisimulation-invariant MSO, and provides a completeness proof using tableaux and Stone duality.

Findings

Fair CTL is the model companion of bisimulation-invariant MSO on trees.

MSO on binary trees is the model companion of binary deterministic fair CTL.

The paper provides a completeness proof for fair CTL combining tableaux and Stone duality.

Abstract

The main focus of this paper is on bisimulation-invariant MSO, and more particularly on giving a novel model-theoretic approach to it. In model theory, a model companion of a theory is a first-order description of the class of models in which all potentially solvable systems of equations and non-equations have solutions. We show that bisimulation-invariant MSO on trees gives the model companion for a new temporal logic, "fair CTL", an enrichment of CTL with local fairness constraints. To achieve this, we give a completeness proof for the logic fair CTL which combines tableaux and Stone duality, and a fair CTL encoding of the automata for the modal {\mu}-calculus. Moreover, we also show that MSO on binary trees is the model companion of binary deterministic fair CTL.