Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
Séminaire organisé par Armaël Gueneau (INRIA Saclay) le 07/03/2024.
Predicting the limit dynamics of automata networks (like deciding if a given network has a fixed point) is a hard problem. We would like to improve our understanding of their attractors on specific families of networks, like disjunctive networks. To do so, we decompose networks into modules, which were defined in my PhD thesis; these modules are automata networks with inputs and outputs. In this presentation we will show what has been done so far using this modular approach, including the definition of output functions (a new way of understanding a network's computation) and an equivalence to the fixed points of a family of cellular automata, culminating in the showcase of a interaction digraph transformation method that's in the works, and could help to prove the dynamical equivalence of families of networks through the transformation of their interaction digraphs.