Automatic structures and graph transformations

In the context of system verification, many formal methods have been developed to analyze safety/reachability properties in order to facilitate their design and to ensure their correctness. Model-checking-based approaches crucially rely on a mathematical model for the behavior of the system. Whereas programs can naturally be represented by state-transition models where states are relatively simple objects, other systems require a much more involved structure to describe a state and as a byproduct a state transtion. We give here two examples of such a situation. (1) In order to reason about information changes in a multi-agent system, it is necessary to consider epistemic states that are graphs and to reflect the effect of an event as an update operation on those graphs (see the update product in Dynamic Epistemic Logic (DEL) [van Ditmarch et al., 2007]). (2) In the Cloud with virtualization, the structure of the network is part of the state [Mensah, 2019] and the dynamics induced by creation/delation/migration of virtual machines impacts the network structure in some way.

In general, when states are complex objects, typically graphs, the whole behavior of the system yields an infinite structure, which critically challenges verification tasks.

The overall objective of this thesis is to make a broad study of finite graph transformations that denote state transitions, and that yield a regular behavior, in particular, of the kind of automatic structures. Indeed, the theory of automatic structures (such as the decidability of first-order logic) has successfully been applied to DEL and shed light on the decidability frontier for the reachability problem in this setting [Bolander et al. 2020]. We thereby expect to obtain elegant results in complexity and decidability/undecidablity of other verification problems, involving complex states and transitions described by graph transformations that generate automatic structures.

For the methodology, we suggest to start with an accurate study of the graph transformations arising from modeling attack penetrations in the Cloud, in the line of [Mensah, 2019]. In particular, we would be interested in establishing which restrictions over the network dynamics (i.e. which kinds of creation/deletion/migration of virtual machines) make these graph transformations amenable to property verification, for yielding e.g. automatic structures. In a next step, we may turn to other applications than penetration in the Cloud, such as graph transformations for data structures evolution in programs. In the long term, by experiencing several settings, we expect to acquire an overall understanding of many aspects in the relationship between graph transformations and automatic structures, possibly leading to the development of generic tools for verification.