Automata Wiki

Learning MultiLogin with Tomte-0.4

Tomte-0.4 can handle fresh output values by way of a Determinizer function. Check the publication for more details on our algorithm. In a learning example Tomte 0.4 was used to infer models for instantiations of Multi-Login Systems with 1, 2 and 3 maximum registered users.

The Learned Models

The abstract models obtained for 1 and 2 user Multi-Login systems correspond to a Mealy Machine that is minimal in terms of the number of states required to describe the system. This is not the case for the 3 user Multi-Login, where because of reordering of state variables, a much greater number of states is found. Nevertheless, learning converges to a final model for which no counterexample is found within a set number of traces.

We show models for the Multi-Login Systems with 2 users. A note is that, depending on the series of counterexamples found, the state machines learned between experiments can differ, both in transitions present and in the number of states. The state machines obtained do pass our testing algorithm so show to be correct. To fortify our notion of correctness, we aim to extend our CADP based based system verification framework to the setting of fresh values.

Fig. 3: Learned SUT Model : Multi-Login with 2 users

Benchmarks

We post benchmarks of learning of 3 instantiations. For each experiment, on the first row you have the average number of inputs of resets used during a learning phase, on the second row you have the standard deviation.