Learning temporal specifications from imperfect traces using Bayesian inference

Artur Mrowca, Martin Nocker, Sebastian Steinhorst, Stephan Günnemann

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

10 Scopus citations


Verification is essential to prevent malfunctioning of software systems. Model checking allows to verify conformity with nominal behavior. As manual definition of specifications from such systems gets infeasible, automated techniques to mine specifications from data become increasingly important. Existing approaches produce specifications of limited lengths, do not segregate functions and do not easily allow to include expert input. We present BaySpec, a dynamic mining approach to extract temporal specifications from Bayesian models, which represent behavioral patterns. This allows to learn specifications of arbitrary length from imperfect traces. Within this framework we introduce a novel extraction algorithm that for the first time mines LTL specifications from such models.

Original languageEnglish
Title of host publicationProceedings of the 56th Annual Design Automation Conference 2019, DAC 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781450367257
StatePublished - 2 Jun 2019
Event56th Annual Design Automation Conference, DAC 2019 - Las Vegas, United States
Duration: 2 Jun 20196 Jun 2019

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X


Conference56th Annual Design Automation Conference, DAC 2019
Country/TerritoryUnited States
CityLas Vegas


  • Bayesian inference
  • Data-driven verification
  • Path merging
  • Specification mining


Dive into the research topics of 'Learning temporal specifications from imperfect traces using Bayesian inference'. Together they form a unique fingerprint.

Cite this