A Pattern Logic for Automata with Outputs

TL;DR

This paper develops a flexible logic framework for automata with outputs, providing decidability conditions, complexity results, and expressiveness analysis for various automata models including finite automata, transducers, and sum-automata.

Contribution

It introduces a parametric logic for automata with outputs, establishing decidability criteria, complexity bounds, and expressive power for multiple automata types.

Findings

Decidability conditions for the model-checking problem.

Complexity results for the three automata models.

Expressiveness of the logic in capturing classical properties.

Abstract

We introduce a logic to express structural properties of automata with string inputs and, possibly, outputs in some monoid. In this logic, the set of predicates talking about the output values is parametric, and we provide sufficient conditions on the predicates under which the model-checking problem is decidable. We then consider three particular automata models (finite automata, transducers and automata weighted by integers -- sum-automata --) and instantiate the generic logic for each of them. We give tight complexity results for the three logics and the model-checking problem, depending on whether the formula is fixed or not. We study the expressiveness of our logics by expressing classical structural patterns characterising for instance finite ambiguity and polynomial ambiguity in the case of finite automata, determinisability and finite-valuedness in the case of transducers and sum-automata. Consequently to our complexity results, we directly obtain that these classical properties can be decided in PTIME.