Categorical Automata Learning Framework

Automata are a well established computational abstraction with a wide range of applications, including modelling and verification of (security) protocols, hardware, and software systems.

In an ideal world, a model would be available before a system or protocol is deployed in order to provide ample opportunity for checking important properties that must hold and only then the actual system would be synthesized from the verified model.

Unfortunately, this is not at all the reality: systems and protocols are developed and coded in short spans of time and if mistakes occur they are most likely found after deployment.

In this context, it has become popular to infer or learn an automaton model from a given system, just by observing its behaviour or response to certain queries. The learned automaton can then be used to ensure the system is complying to desired properties or to detect bugs and design possible fixes.

Modular design and development

CALF allows for the modular design and development of automata learning algorithms. In order to do so, it relies on general mathematical frameworks, such as category-theory and the theory of nominal sets. This ensures applicability to a broad class of systems.

Correctness-by-construction

CALF facilitates correctness proofs of automata learning algorithms. It provides a general and principled account of crucial aspects of algorithms, such as data structures and their properties.