A pattern logic for automata with outputs

Nicolas Mazzocchi
Friday, 11 May, 2018 - 16:00
ULB La Plaine NO, Salle Solvay
In this presentation, we introduce a logic to express path properties of automata with string inputs and outputs in any monoid. Intended to model various automata formalisms, such as transducers or automata weighted in Z, we provide complexity results with respect to the model-checking problem. We provide tight complexity results for monoids of interests, such as the free monoid, or the monoid (Z, +, 0), depending on whether the formula is, fixed or not. In particular, we introduce two fragments for these two monoids respectively, which both admit PTime model-checking when the formula is fixed. This allows us to recover many known PTime complexity results to test transducer properties such as the twinning property, the functionality, the finite-valuedness property, as well as properties of automata with weights in Z, such as functionality, finite-ambiguity or determinisability.