Weighted Automata and Logics for Infinite Nested Words

TL;DR

This paper extends the theory of nested words by developing weighted automata and MSO logics for infinite nested structures, incorporating average and discounted weights, and demonstrating their expressive equivalence.

Contribution

It introduces weighted automata and logics for infinite nested words with valuation monoids, unifying average, discounted, and classical weights, and proves their expressive equivalence.

Findings

Weighted automata and MSO logics are equivalent in expressive power.

Fragments of weighted logics can be transformed into each other.

The framework unifies classical and quantitative weights in nested words.

Abstract

Nested words introduced by Alur and Madhusudan are used to capture structures with both linear and hierarchical order, e.g. XML documents, without losing valuable closure properties. Furthermore, Alur and Madhusudan introduced automata and equivalent logics for both finite and infinite nested words, thus extending B\"uchi's theorem to nested words. Recently, average and discounted computations of weights in quantitative systems found much interest. Here, we will introduce and investigate weighted automata models and weighted MSO logics for infinite nested words. As weight structures we consider valuation monoids which incorporate average and discounted computations of weights as well as the classical semirings. We show that under suitable assumptions, two resp. three fragments of our weighted logics can be transformed into each other. Moreover, we show that the logic fragments have the same expressive power as weighted nested word automata.