KnoBAB

A fast LTLf Log-SAT Solver and miner with Data Payload

KnoBAB provides an ecosystem for temporal data analysis, supporting both multivariate time series analysis and log data. Both of these data models are represented into an internal columnar database enabling fast data querying and mining, while outperforming state of the art algorithms.

Bechmarks showing that our solutions outperform state of the art data-aware formal verification (left: (Bergami et al., 2023)), formal synthesis (center: (Bergami, 2023)), and multivariate time series classification (right: (Bergami et al., 2025)) solutions.
Temporal data is loaded into a columnar database (above), while declarative queries are rewritten into algebraic temporal operators (below) (Bergami et al., 2023).

While specification mining, formal verification, and formal synthesis tasks need the prompt interaction with C++ code, we are working towards fully-supporting the Multivariate Time Series classification task in Python, for which we now provide a separate Python pipeline via EMeriTAte.

Invited Talks and Presentations

References

2025

  1. Best Paper Award
    ../KnoBAB2.png
    Predicting Dyskinetic Events through Verified Multivariate Time Series Classification
    Giacomo Bergami, Emma Packer, Kirsty Scott, and 1 more author
    In Database Engineered Applications, Apr 2025

2023

  1. Inf.
    ../KnoBAB2.png
    Quickening Data-Aware Conformance Checking through Temporal Algebras
    Giacomo BergamiSamuel Appleby, and Graham Morgan
    Information, Apr 2023
  2. GRADES-NDA
    ../KnoBAB2.png
    Fast Synthetic Data-Aware Log Generation for Temporal Declarative Models
    Giacomo Bergami
    In Proceedings of the 6th Joint Workshop on Graph Data Management Experiences & Systems (GRADES) and Network Data Analytics (NDA), Seattle, WA, USA, Apr 2023