# Logics for Reversible Regular Languages and Semigroups with Involution

## TL;DR

This paper develops logical frameworks using MSO and FO with specific predicates to characterize reversible regular languages, extending classical connections to semigroups with involution and highlighting unique requirements for FO with neighbour relation.

## Contribution

It introduces new logical characterizations for reversible regular languages and extends the algebraic connections to involutive semigroups, revealing differences in FO logic.

## Key findings

- MSO and FO logics with 'between' and 'neighbour' characterize reversible regular languages.
- Standard MSO-FO and semigroup correspondences extend to involutive semigroups.
- Additional equations are necessary for FO with neighbour to characterize the class.

## Abstract

We present MSO and FO logics with predicates `between' and `neighbour' that characterise various fragments of the class of regular languages that are closed under the reverse operation. The standard connections that exist between MSO and FO logics and varieties of finite semigroups extend to this setting with semigroups extended with an involution. The case is different for FO with neighbour relation where we show that one needs additional equations to characterise the class.