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.
A temporal model describes processes as a sequence of observable events characterised by distinguishable actions in time. Conformance checking allows these models to determine whether any sequence of temporally ordered and fully-observable events complies with their prescriptions. The latter aspect leads to Explainable and Trustworthy AI, as we can immediately assess the flaws in the recorded behaviours while suggesting any possible way to amend the wrongdoings. Recent findings on conformance checking and temporal learning lead to an interest in temporal models beyond the usual business process management community, thus including other domain areas such as Cyber Security, Industry 4.0, and e-Health. As current technologies for accessing this are purely formal and not ready for the real world returning large data volumes, the need to improve existing conformance checking and temporal model mining algorithms to make Explainable and Trustworthy AI more efficient and competitive is increasingly pressing. To effectively meet such demands, this paper offers KnoBAB, a novel business process management system for efficient Conformance Checking computations performed on top of a customised relational model. This architecture was implemented from scratch after following common practices in the design of relational database management systems. After defining our proposed temporal algebra for temporal queries (xtLTLf), we show that this can express existing temporal languages over finite and non-empty traces such as LTLf. This paper also proposes a parallelisation strategy for such queries, thus reducing conformance checking into an embarrassingly parallel problem leading to super-linear speed up. This paper also presents how a single xtLTLf operator (or even entire sub-expressions) might be efficiently implemented via different algorithms, thus paving the way to future algorithmic improvements. Finally, our benchmarks highlight that our proposed implementation of xtLTLf (KnoBAB) outperforms state-of-the-art conformance checking software running on LTLf logic.
GRADES-NDA
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
Business Process Management algorithms are heavily limited by suboptimal algorithmic implementations that cannot leverage state-of-the-art algorithms in the field of relational and graph databases. The recent interest in this discipline for various IT sectors (cyber-security, Industry 4.0, and e-Health) calls for defining new algorithms improving the performance of existing ones. This paper focuses on generating several traces collected in a log from declarative temporal models by pre-emptively representing those as a specific type of finite state automaton: we show that this task boils down to a single-source multi-target graph traversal on such automaton where both the number of distinct paths to be visited as well as their length are bounded. This paper presents a novel algorithm running in polynomial time over the size of the declarative model represented as a graph and the desired log’s size. The final experiments show that the resulting algorithm outperforms the state-of-the-art data-aware and dataless sequence generations in business process management.
We would like to use third party cookies and scripts to improve the functionality of this website.ApproveDenyMore info