Monadic second order logic as the model companion of temporal logic

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-equ...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2016-05
Main Authors: Ghilardi, Silvio, van Gool, Samuel J
Format: Article
Language:English
Subjects:
Companion stars
Invariants
Mathematical models
Temporal logic
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422