Performance Evaluation
All experiments were conducted on the Dell Lattitude 5410. PyPy 3.9 was used instead of CPython. With CPython, all experiments will take several times (3-6x) longer.
The runtime of the deterministic L* with respect to the automaton's size (left) and alphabet size (right). In the first scenario, the alphabet size was set to 10, while in the second scenario number of states was set to 1000. We see a linear increase in runtime with respect to the automaton size. In the right graph, we see an interesting trend. From the alphabet size of 50 onward, DFA's are less affected by the increase in alphabet size than Mealy and Moore machined. We used Rivest-Shapiro counterexample processing and no caching.
When inferring real-world systems, minimal overhead/computation introduced by AALpy pales in comparison to the interaction with the system. Therefore, when inferring deterministic systems use of caching is very much advised.
To evaluate our reimplementation of L*Mdp, we used the same model-checking experiments as in the evaluation of the original Java implementation of L*Mdp. We learned four MDP models with both AALpy and the Java implementation, model checked them, while repeating each experiment
Following figure shows the average runtime and the average model-checking errors measured in the experiments.
The latter is the average absolute difference between probabilistic model-checking on a learned model and the true model. We can see that AALpy and the Java implementation are generally similarly fast and produce similarly accurate models. Although we used the same configuration for both implementations, there is some difference, like for the shared coin model.
These differences can be attributed to implementation details, like improvements in AALpy and a different, computationally expensive equivalence query in the Java implementation. The experiments demonstrate that AALpy provides the functionality of the prototypical Java implementation.