@inbook{df19546f24654eb8bd2e599d06feb87a,
title = "Synchronous or Alternating?: LTL Black-Box Checking of Mealy Machines by Combining the LearnLib and LTSmin",
abstract = "Mealy machines transduce inputs to outputs, based on finite memory. They are often used to model reactive systems. The requirements on their behaviour can be specified by formulas in Linear-time Temporal Logic. We will study two interpretations of LTL for Mealy machines: the synchronous semantics, where inputs and outputs occur simultaneously; and the alternating semantics, where inputs and outputs strictly alternate. We define and study Mealy-robust LTL properties, which are insensitive to which of these interpretations is chosen. The motivating application is in the context of black-box checking: Given the interface to some reactive system, one would like to test that a particular LTL property holds. To this end, we combine active automata learning with model checking into sound black-box checking. Here the LTL properties are already checked on intermediate hypotheses, in order to speed up the learner. Finally, we perform an experiment on the Mealy machines provided by the RERS challenge (Rigorous Examination of Reactive Systems). We investigate how many LTL properties from the RERS challenges in 2016 and 2017 are actually robust.",
author = "{van de Pol}, Jaco and Jeroen Meijer",
year = "2019",
month = jan,
day = "1",
doi = "10.1007/978-3-030-22348-9_24",
language = "English",
isbn = "978-3-030-22347-2",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "417--430",
editor = "Tiziana Margaria and Susanne Graf and Larsen, {Kim G.}",
booktitle = "Models, Mindsets, Meta: The What, the How, and the Why Not?",
address = "Germany",
}