A Pattern Logic for Automata with Outputs

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. We then consider three particular automata models (finite automata, transducers and automata weighted by integers here called sum-automata) and instantiate the generic logic for each of them. We give tight complexity results for the three logics with respect to 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. As a consequence of our complexity results, we directly obtain that these classical properties can be decided in polynomial time.