LTL on Weighted Finite Traces: Formal Foundations and Algorithms
Authors: Carmine Dodaro, Valeria Fionda, Gianluigi Greco
IJCAI 2022 | Conference PDF | Archive PDF | Plain Text | 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). |