Sound Black-Box Checking in the LearnLib

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
LanguageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings
EditorsAaron Dutle, César A. Muñoz, Anthony Narkawicz
Place of PublicationCham
PublisherSpringer
Pages349-366
Number of pages18
ISBN (Electronic)978-3-319-77935-5
ISBN (Print)978-3-319-77934-8
DOIs
StatePublished - 11 Mar 2018

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10811
ISSN (Print)0302-9743

Fingerprint

Acoustic waves
Learning algorithms
Finite automata
Application programming interfaces (API)
Experiments
Problem-Based Learning

Cite this

Meijer, J., & van de Pol, J. (2018). Sound Black-Box Checking in the LearnLib. In A. Dutle, C. A. Muñoz, & A. Narkawicz (Eds.), NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings (pp. 349-366). (Lecture Notes in Computer Science; Vol. 10811). Cham: Springer. DOI: 10.1007/978-3-319-77935-5_24
Meijer, Jeroen ; van de Pol, Jaco. / Sound Black-Box Checking in the LearnLib. NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. editor / Aaron Dutle ; César A. Muñoz ; Anthony Narkawicz. Cham : Springer, 2018. pp. 349-366 (Lecture Notes in Computer Science).
@inproceedings{bc2875148465462f9c30d3662afb6afa,
title = "Sound Black-Box Checking in the LearnLib",
abstract = "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.",
author = "Jeroen Meijer and {van de Pol}, Jaco",
year = "2018",
month = "3",
day = "11",
doi = "10.1007/978-3-319-77935-5_24",
language = "English",
isbn = "978-3-319-77934-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "349--366",
editor = "Aaron Dutle and Mu{\~n}oz, {C{\'e}sar A.} and Anthony Narkawicz",
booktitle = "NASA Formal Methods",

}

Meijer, J & van de Pol, J 2018, Sound Black-Box Checking in the LearnLib. in A Dutle, CA Muñoz & A Narkawicz (eds), NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10811, Springer, Cham, pp. 349-366. DOI: 10.1007/978-3-319-77935-5_24

Sound Black-Box Checking in the LearnLib. / Meijer, Jeroen; van de Pol, Jaco.

NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. ed. / Aaron Dutle; César A. Muñoz; Anthony Narkawicz. Cham : Springer, 2018. p. 349-366 (Lecture Notes in Computer Science; Vol. 10811).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - Sound Black-Box Checking in the LearnLib

AU - Meijer,Jeroen

AU - van de Pol,Jaco

PY - 2018/3/11

Y1 - 2018/3/11

N2 - 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.

AB - 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.

UR - https://github.com/Meijuh/NFM2018BBC

U2 - 10.1007/978-3-319-77935-5_24

DO - 10.1007/978-3-319-77935-5_24

M3 - Conference contribution

SN - 978-3-319-77934-8

T3 - Lecture Notes in Computer Science

SP - 349

EP - 366

BT - NASA Formal Methods

PB - Springer

CY - Cham

ER -

Meijer J, van de Pol J. Sound Black-Box Checking in the LearnLib. In Dutle A, Muñoz CA, Narkawicz A, editors, NASA Formal Methods: 10th International Symposium, NFM 2018, Newport News, VA, USA, April 17-19, 2018, Proceedings. Cham: Springer. 2018. p. 349-366. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-77935-5_24