|title:||Smart composition of communicating automata with AI|
|keywords:||Model Checking, Artificial Intelligence, Space optimisation|
|topics:||Algorithms and Data Structures|
Carlos Esteban Budde
Communicating automata (e.g. Interactive Markov Chains) are graphical models commonly used to describe system components. In the field of model checking, a common task is to take all the automata which model such components of a large system, and compose them into a single automaton describing the entire system. One approach is to do compositional aggregation. Here, one selects some automata of the system, composes them, then performs a minimization to convert the composed automaton into a smaller automaton with the same behaviour, and then repeats this until all automata have been composed.
The order in which these automata are composed can make a huge difference. When two automata are composed, the size of the result can be large, and can take too much memory. The opportunities for minimization depend heavily on the choice of which automata are composed, so bad orders can make even simple models impossible to analyse on a normal machine. Take an analysis tool in which these automata describe the faults of real system components (and they are the nodes of a so-called Fault Tree). The order of the automata composition currently follows an undocumented heuristic by an external tool. This heuristic is generally good, but improvement is possible.
Research whether an Artificial Intelligence approach can find a better strategy to compose the automata in a Fault Tree and minimize the intermediate models. This could be a smart heuristic, a machine-learning algorithm, or even a graph-based algorithm.
The solution may use static features of the Fault Tree (e.g. composing elements that are not connected in the tree is rarely a good idea) or static features of the automata (e.g. automata that communicate a lot might be good candidates). The solution may also try to predict the size of the composition by using what are called dynamic features: you can start to compose two automata, but only partially (up to a certain depth, for example), and use the shape of this partial composition to predict the size of the entire composition.