Library for translating Linear-time Temporal Logic (LTL) and Linear Dynamic Logic (LDL) formulas with finite-trace semantics to automata, so as to perform satisfiability and validity reasoning tasks in the finite-trace setting (Java, 13K+ LOC);
Library for the translation of First-order Linear-time Temporal Logic (FO-LTL) to automata, under finite-domain assumption (Java, 18K+ LOC);
A process model discovery tool which, from a log, returns a "fuzzy" Petri net representing the process (Java, 8K+ LOC).