Wednesday 14 May 2025
Venue: LIGM, Marne-la-Vallée
Note the unusual time and venue. For more information see at GT DAAL / Venue.
For planning purposes, please indicate your participation at https://framadate.org/HEqJTiuzJs8JIyUB
9:30 Barbara König (online): Graph Automata and Automaton Functors
Abstract:
We generalize Courcelle's recognizable graph languages and results on monadic second-order logic to more general structures.
We give a category-theoretical characterization of recognizability. A recognizable subset of arrows in a category is defined via a functor into the category of relations on finite sets. This can be seen as a straightforward generalization of finite automata and we show how to obtain graph automata - accepting recognizable graph languages - by applying the theory to the category of cospans of graphs.
We also introduce a simple logic that allows to quantify over the subobjects of a categorical object and we show that, for the category of graphs, this logic is equally expressive as monadic second-order graph logic (MSOGL). Furthermore, we explain that in the more general setting of hereditary pushout categories, a class of categories closely related to adhesive categories, we can recover Courcelle's result that every MSOGL-expressible property is recognizable.
The talk concludes by reviewing a practical implementation of graph automata with applications to the verification of graph transformation systems.
10:30 Break
11:00 Denis Kuperberg (present): Explorable Automata
Abstract:
We define the class of explorable automata on finite or infinite words. This is a generalization of History-Deterministic (HD) automata, where this time non-deterministic choices can be resolved by building finitely many simultaneous runs instead of just one.
We show that recognizing HD parity automata of fixed index among explorable ones is in PTIME, thereby giving a strong link between the two notions. We then show that recognizing explorable automata is EXPTIME-complete, in the case of finite words or parity automata up to index [0,2]. Additionally, we define the notion of ω-explorable automata on infinite words, where countably many runs can be used to resolve the non-deterministic choices. We show EXPTIME-completeness for ω-explorability of automata on infinite words for the safety and co-Büchi acceptance conditions.
We finally characterize the expressivity of (ω-)explorable automata with respect to the parity index hierarchy.
We leave open the decidability of explorability for [1,3]-automata and ω- explorability for Büchi automata, both equivalent to the general case of arbitrary acceptance conditions.
This is joint work with Emile Hazard and Olivier Idir (short version CSL 2023, long version submitted to LMCS).