A generic characterization of generalized unary temporal logic and two-variable first-order logic
Abstract
We investigate an operator on classes of languages. For each class , it outputs a new class associated with a variant of two-variable first-order logic equipped with a signature built from . For , we get the variant equipped with the linear order. For , we get the variant , which also includes the successor. If consists of all Boolean combinations of languages where is a letter, we get the variant , which also includes "between relations". We prove a generic algebraic characterization of the classes . It smoothly and elegantly generalizes the known ones for all aforementioned cases. Moreover, it implies that if has decidable separation (plus mild properties), then has a decidable membership problem. We actually work with an equivalent definition of \fodc in terms of unary temporal logic. For each class , we consider a variant of unary temporal logic whose future/past modalities depend on and such that . Finally, we also characterize and , the pure-future and pure-past restrictions of . These characterizations as well imply that if \Cs is a class with decidable separation, then and have decidable membership.
Cite
@article{arxiv.2307.09349,
title = {A generic characterization of generalized unary temporal logic and two-variable first-order logic},
author = {Thomas Place and Marc Zeitoun},
journal= {arXiv preprint arXiv:2307.09349},
year = {2023}
}
Comments
Extended version of CLS 2024 paper