$\omega$-Forest Algebras and Temporal Logics

TL;DR

This paper employs algebraic methods for infinite tree languages to characterize and analyze the expressive power of temporal logics like EF and cEF, providing effective algebraic descriptions.

Contribution

It introduces algebraic characterizations for EF and cEF temporal logics using $-forest algebras, extending previous algebraic frameworks to these logics.

Findings

Effective algebraic characterizations of EF and cEF logics.

Extension of algebraic framework to infinite trees.

Enhanced understanding of temporal logic expressiveness.

Abstract

We use the algebraic framework for languages of infinite trees introduced in [4] to derive effective characterisations of various temporal logics, in particular the logic EF (a fragment of CTL) and its counting variant cEF.