Synchronous or Alternating? LTL Black-Box Checking of Mealy Machines by Combining the LearnLib and LTSmin

Jaco van de Pol*, Jeroen Meijer

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

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.

Original languageEnglish
Title of host publicationModels, Mindsets, Meta: The What, the How, and the Why Not?
Subtitle of host publicationEssays Dedicated to Bernhard Steffen on the Occasion of His 60th Birthday
EditorsTiziana Margaria, Susanne Graf, Kim G. Larsen
Place of PublicationCham
PublisherSpringer
Pages417-430
Number of pages14
ISBN (Electronic)978-3-030-22348-9
ISBN (Print)978-3-030-22347-2
DOIs
Publication statusPublished - 1 Jan 2019

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume11200
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameTheoretical Computer Science and General Issues
PublisherSpringer

Fingerprint Dive into the research topics of 'Synchronous or Alternating? LTL Black-Box Checking of Mealy Machines by Combining the LearnLib and LTSmin'. Together they form a unique fingerprint.

Cite this