Quantitative Automata Learning

Many important network properties such as congestion and fault tolerance are dependent on some form of randomisation or weights. Automata models to represent these will have to be probabilistic or, more generally, weighted. I will design novel active learning algorithms for probabilistic and weighted automata that go much beyond existing ones, which only cover a limited class of probabilistic behaviours (namely the deterministic) and weighted behaviors (the semiring from which the weights are drawn is either a field or a principal ideal domain). As the learned models will be quantitative, we will also develop behavioral distances to measure the quality of the learned models. Both these research lines – algorithms and distances – will be rooted in strong foundational understanding of the models. In particular, the categorical learning framework developed in the last years will serve as an ideal starting point for this strand.

Concurrent Automata Learning

The highly distributed nature of networks gives rise to behaviors that are complex and subtle to analyse, as they are caused by interactions between network components and multiple packets in a concurrent fashion. In recent work, we have proposed a language, together with a denotational semantics and automata, to capture concurrent behavior. We will design novel algorithms to learn (subclasses of) these concurrent automata and investigate model checking algorithms. We will exploit the limits of the framework and integrate the algorithms from this strand with the previous one, yielding algorithms for models with both concurrent and probabilistic behavior. This integration, and the potential limitations, will be guided by the categorical understanding of the algorithms, which will also provide modular proofs of correctness.

Model Learning for Network Verification

The current progress on automated verification tools for black-box network programs is still nascent. To ease the use of verification by network programmers and operators, who want to have automated alerts for potential problems and then reason about the precise behavior that might lead to bugs, we will develop a framework that makes the techniques and tools from the previous strands available for learning models of network programs automatically. We will develop a tailor-made tool-suite of tests for network properties as well as abstraction and concretization algorithms that enable the conversion of concrete network tests into more abstract elements to be used in the model and, vice-versa, enable the generation of concrete tests that can be used to learn the network behavior.