Decomposition of automata and applications to logic

My thesis topic is to find decomposition of models of computation in terms of simpler structures. One of the cornerstones of this area is the celebrated Krohn-Rhodes decomposition theorem, named after the two researchers who discovered it in the 1960s. The theorem in its original form is algebraic in nature, and deals with transformation monoids or just monoids. However, semigroup theory has deep connections with automata and language theory, and it provides many algebraic tools, theorems and insights to reason about automata and languages. As a consequence of these connections, the Krohn-Rhodes theorem essentially gives a cascade decomposition of any finite automata (DFA) in terms of ‘‘simpler" DFAs. In particular, if we are dealing with first order logic (FOL) or linear temporal logic (LTL) formulas, then the the simpler DFAs are just two state reset devices. The theorem is also a powerful, yet easy to use inductive tool to prove several non-trivial theorems in language theory e.g- Kamp's theorem.

Our focus is on finding similar decomposition results in more general settings like distributed traces and countable linear orderings. Countable words are words whose underlying linear ordering is countable. Recently Carton, Colcombet and Puppis came up with an algebraic structure suitable for recognizing regular languages of countable words. We set up block product operation over these structures and proved decomposition results for FOL and LTL definable languages. Our results are published in LICS 2019.

Distributed computation is an exciting challenge for the computer science community. It is ubiquitous in nature, but modelling it formally and proving even classical theorems of word languages in this setting often turn out to be complicated. Trying to naively lift the Krohn-Rhodes theorem to this setting breaks down very fast. We have some preliminary results in this area.

Our next goal is to extend these results to more general settings