Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
LTL on Weighted Finite Traces: Formal Foundations and Algorithms
Authors: Carmine Dodaro, Valeria Fionda, Gianluigi Greco
IJCAI 2022 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Moreover, a reasoner for LTLf on weighted traces is presented, and its performance are assessed on benchmark data. |
| Researcher Affiliation | Academia | Carmine Dodaro , Valeria Fionda and Gianluigi Greco Department of Mathematics and Computer Science, University of Calabria |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks. |
| Open Source Code | Yes | WELTL, the benchmark data and details on the (theoretical/experimental) results are available as Supplementary Material. |
| Open Datasets | Yes | For the evaluation, we used a benchmark taken from the business process domain, namely a dataset of 109 satisfiable DECLARE formulas [van der Aalst et al., 2009] obtained by mining all DECLARE constraints that hold on a number of logs made available by the IEEE Task-Force on Process Mining (http://datacentrum.3tu.nl). |
| Dataset Splits | No | The paper describes how cost bounds were set for experiments but does not provide specific train/validation/test dataset splits. |
| Hardware Specification | Yes | Experiments have been carried out on a Intel CPU 2,4 GHz with 16GB RAM. |
| Software Dependencies | No | The paper mentions 'the ASP engine clingo [Gebser et al., 2018]' but does not provide a specific version number for it or other software dependencies. |
| Experiment Setup | Yes | For each formula, we randomly generated the variable weights in the intervals [1, 5] and [1, 10] and considered all combinations of max and + operators, thus ending up with a dataset of 872 weighted settings. Moreover, for each weighted setting, we considered four different cost bounds obtained as follows: (i) we compute an arbitrary model π; (ii) we build a trace π whose length n is the same as π and such that π i=V for each i {0, ..., n 1}; (iii) we set the cost bounds to the 25%, 50%, 75% and 90% of v(π ). ...Time and memory were limited to 600 seconds and 15GB, respectively. In particular, we first run WELTLbf (with 300 seconds of timeout); and if no solution has been returned, then we run WELTLdf (again with the same timeout). |