In Black-Box Checking (BBC) incremental hypotheses of a system are learned in the form of finite automata. On these automata LTL formulae are verified, or their counterexamples validated on the actual system. We extend the LearnLib’s system-under-learning API for sound BBC, by means of state equivalence, that contrasts the original proposal where an upper-bound on the number of states in the system is assumed. We will show how LearnLib’s new BBC algorithms can be used in practice, as well as how one could experiment with different model checkers and BBC algorithms. Using the RERS 2017 challenge we provide experimental results on the performance of all LearnLib’s active learning algorithms when applied in a BBC setting. The performance of learning algorithms was unknown for this setting. We will show that the novel incremental algorithms TTT, and ADT perform the best.
|Title of host publication||NASA Formal Methods|
|Subtitle of host publication||10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings|
|Editors||Aaron Dutle, César A. Muñoz, Anthony Narkawicz|
|Place of Publication||Cham|
|Number of pages||18|
|Publication status||Published - 11 Mar 2018|
|Name||Lecture Notes in Computer Science|