A Short Note on Infinite Union/Intersection of Omega Regular Languages

TL;DR

This paper demonstrates that omega regular languages are not closed under infinite union and intersection, and explores adding quantifiers to temporal logics to increase expressiveness, which leads to undecidability issues.

Contribution

It reveals the limitations of omega regular languages under infinite operations and proposes an extension to temporal logic, highlighting the trade-off between expressiveness and decidability.

Findings

Omega regular languages are not closed under infinite union and intersection.

Adding quantifiers to temporal logic increases expressiveness but causes undecidability.

The undecidability persists even in limited fragments of the extended logic.

Abstract

We in this paper show that omega regular languages are not closed under infinite union and intersection. As an attempt, we propose to add step variables and quantifiers to temporal logics to enhance the expressiveness of the underlying logic. We also show that doing this would cause undecidability in satisfiability, even if for a rather limited fragment of temporal logic.