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

Learning algorithms
Finite automata
Application programming interfaces (API)
Experiments

Cite this

Meijer, J., & Pol, J. V. D. (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; Pol, Jaco van de / Sound Black-Box Checking in the LearnLib.

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: Scientific - peer-reviewConference contribution

@inbook{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 Pol, {Jaco van de}",
year = "2018",
month = "3",
doi = "10.1007/978-3-319-77935-5_24",
isbn = "978-3-319-77934-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "349--366",
editor = "Aaron Dutle and Muñoz, {César A.} and Anthony Narkawicz",
booktitle = "NASA Formal Methods",

}

Meijer, J & Pol, JVD 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; Pol, Jaco van de.

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: Scientific - peer-reviewConference contribution

TY - CHAP

T1 - Sound Black-Box Checking in the LearnLib

AU - Meijer,Jeroen

AU - Pol,Jaco van de

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

ER -

Meijer J, Pol JVD. 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