Logic and Branching Automata

TL;DR

This paper explores the logical properties of branching automata, proving closure under complementation and establishing an expressive logic, P-MSO, that precisely characterizes these automata, leading to decidability results.

Contribution

It introduces P-MSO logic for branching automata and proves its equivalence, enabling effective decision procedures for their theories.

Findings

Languages recognized by branching automata are closed under complementation.

P-MSO logic is as expressive as branching automata.

The P-MSO theory of finite N-free posets is decidable.

Abstract

In this paper we study the logical aspects of branching automata, as defined by Lodaya and Weil. We first prove that the class of languages of finite N-free posets recognized by branching automata is closed under complementation. Then we define a logic, named P-MSO as it is a extension of monadic second-order logic with Presburger arithmetic, and show that it is precisely as expressive as branching automata. As a consequence of the effectiveness of the construction of one formalism from the other, the P-MSO theory of the class of all finite N-free posets is decidable.