Learning Weighted Finite Automata over the Max-Plus Semiring and its Termination

TL;DR

The paper tackles the problem of actively learning weighted finite automata over the max-plus semiring using L*-style methods. It identifies a consistency failure in semiring-generic extensions and introduces column-closedness as a robust dual to row-closedness, ensuring faithful WFAs can be learned; it also proves termination for a meaningful class of max-plus WFAs (notably those with rational weights) while acknowledging non-termination in general. The proposed algorithm builds and enforces row- and column-closed Hankel subblocks to obtain a faithful WFA, and it is contrasted with existing approaches that may stall or yield unfaithful hypotheses. The work thereby advances semiring-agnostic automata learning, clarifying when and how max-plus WFAs can be learned and identifying practical termination guarantees and their limitations. Overall, the findings offer a principled path to faithful max-plus WFA learning and highlight where further work is needed to broaden termination guarantees and minimality results.

Abstract

Active learning of finite automata has been vigorously pursued for the purposes of analysis and explanation of black-box systems. In this paper, we study an L*-style learning algorithm for weighted automata over the max-plus semiring. The max-plus setting exposes a "consistency" issue in the previously studied semiring-generic extension of L*: we show that it can fail to maintain consistency of tables, and can thus make equivalence queries on obviously wrong hypothesis automata. We present a theoretical fix by a mathematically clean notion of column-closedness. We also present a nontrivial and reasonably broad class of weighted languages over the max-plus semiring in which our algorithm terminates.

Figures (2)

• Figure 1: Our L*-style algorithm for the max-plus semiring. Dashed lines indicate interaction with the oracles. Rudimentarily speaking, a Hankel mask is the size of a table, and a Hankel subblock $H_{(P,S)}$ is a table. The existing algorithms check only row-closedness and not column-closedness.
• Figure 2: L*-style algorithms, an outline. Dashed lines indicate interaction with the oracles. Algorithms differ in what exactly they require in "closedness" and "consistency."

Theorems & Definitions (7)

• definition 1: rational WFA
• proof
• proof
• proof
• proof
• proof
• proof : of Theorem \ref{['thm:term']}