Sound Black-Box Checking in the LearnLib

Jeroen Meijer, Jaco van de Pol

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    4 Citations (Scopus)
    123 Downloads (Pure)

    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
    Publication statusPublished - 11 Mar 2018

    Publication series

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

    Fingerprint

    Black Box
    Acoustic waves
    Learning algorithms
    Finite automata
    Learning Algorithm
    Application programming interfaces (API)
    Incremental Algorithm
    Active Learning
    Finite Automata
    Automata
    Counterexample
    Equivalence
    Sound
    Upper bound
    Unknown
    Experiments
    Experimental Results
    Experiment

    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. https://doi.org/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. https://doi.org/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 contributionAcademicpeer-review

    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

    UR - http://www.scopus.com/inward/record.url?scp=85045343611&partnerID=8YFLogxK

    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

    A2 - Dutle, Aaron

    A2 - Muñoz, César A.

    A2 - Narkawicz, Anthony

    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). https://doi.org/10.1007/978-3-319-77935-5_24