Rafał Stefański

Highlights Conference 2025 Conference Abstract

Polyregular Model Checking

• Rafał Stefański

Highlights Conference 2023 Conference Abstract

Monads, comonads, and transducers

• Rafał Stefański

Regular languages are one of the most fundamental concepts in the area of formal language theory. In the recent decades, there has been an ongoing effort to extend the definition of regularity to structures more complex than finite words. Examples include infinite words, as well as finite and infinite trees. A recently developed line of research (see references at the end of the paper) is to find a common framework that would encapsulate (at least a significant portion of) these various generalizations. The approach proposed in the cited publications is to define regularity in terms of monads and their algebras – the framework proposes a definition of regularity for languages that are subsets of MΣ, where M is a monad, and Σ is a finite alphabet. In this presentation, I would like to discuss a possible extension of this framework for studying transducers. For this purpose, I am going to consider functors that simultaneously exhibit both the structure of a monad and of a comonad. It turns out that for such functors one can define a class of recognizable functions of type MΣ → MΓ, which (depending on the chosen M) can encompass deterministic Mealy machines (both left-to-right and right-to-left), letter-to-letter rational functions, and some classes of transductions for structures other than words. In the talk, I plan to discuss what properties of M are required, to ensure that the class of its transductions is closed under compositions, and to discuss potential directions for future work. REFERENCES: Bojańczyk, Mikołaj. "Recognizable languages over monads. " Developments in Language Theory: 19th International Conference, DLT 2015, Liverpool, UK, July 27-30, 2015, Proceedings. . Cham: Springer International Publishing, 2015. Bojańczyk, Mikołaj. "Languages recognized by finite semigroups, and their generalizations to objects such as trees and graphs, with an emphasis on definability in monadic second-order logic. " arXiv e-prints (2020): arXiv-2008. Bojańczyk, Mikołaj, Bartek Klin, and Julian Salamanca. "Monadic monadic second order logic. " arXiv preprint arXiv: 2201. 09969 (2022). Contributed talk given by Rafał Stefański

Highlights Conference 2021 Conference Abstract

Single-use register automata and orbit-finite monoids for total-order atoms

• Rafał Stefański

Single-use register automata are a variant of register automata (in the style of Kaminski & Francez) in which every read access to register destroys its contents. Last year at Highlights, I discussed single-use register automata for atoms which can only be compared for equality. This year, I will discuss atoms with total orders. One notable difference between these two kinds of atoms is that with equality only, single-use automata recognise the same languages as orbit-finite semigroups, while in the presence of total order, single-use automata correspond to an interesting subclass of orbit-finite semigroups. This is based on joint work with Mikołaj Bojańczyk and Nathan Lhote.

Highlights Conference 2020 Conference Abstract

Single-use automata and transducers for infinite alphabets

• Rafał Stefański

Our starting point are register automata for data words, in the style of Kaminski and Francez. We study the effects of the single-use restriction, which says that a register is emptied immediately after being used. We show that under the single-use restriction, the theory of automata for data words becomes much more robust. The main results are: (a) five different machine models are equivalent as language acceptors, including one-way and two-way single-use register automata; (b) one can recover some of the algebraic theory of languages over finite alphabets, including a version of the Krohn-Rhodes Theorem; (c) there is also a robust theory of transducers, with four equivalent models, including two-way single use transducers and a variant of streaming string transducers for data words. These results are in contrast with automata for data words without the single-use restriction, where essentially all models are pairwise non-equivalent This is a joint work with Mikołaj Bojańczyk.