Toggle Main Menu Toggle Search

Open Access padlockePrints

DECLAREd: A Polytime LTLf Fragment

Lookup NU author(s): Dr Giacomo BergamiORCiD

Downloads


Licence

This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0).


Abstract

This paper considers a specification rewriting meachanism for a specific fragment of Linear Temporal Logic for Finite traces, DECLAREd, working through an equational logic and rewriting mechanism under customary practitioner assumptions from the Business Process Management literature. By rewriting the specification into an equivalent formula which might be easier to compute, we aim to streamline current state-of-the-art temporal artificial intelligence algorithms working on temporal logic. As this specification rewriting mechanism is ultimately also able to determine with the provided specification is a tautology (always true formula) or a formula containing a temporal contradiction, by detecting the necessity of a specific activity label to be both present and absent within a log, this implies that the proved mechanism is ultimately a SAT-solver for DECLAREd. We prove for the first time, to the best of our knowledge, that this fragment is a polytime fragment of LTLf, while all the previously-investigated fragments or extensions of such a language were in polyspace. We test these considerations over formal synthesis (Lydia), SAT-Solvers (AALTAF) and formal verification (KnoBAB) algorithms, where formal verification can be also run on top of a relational database and can be therefore expressed in terms of relational query answering. We show that all these benefit from the aforementioned assumptions, as running their tasks over a rewritten equivalent specification will improve their running times, thus motivating the pressing need of this approach for practical temporal artificial intelligence scenarios. We validate such claims by testing such algorithms over a Cybersecurity dataset.


Publication metadata

Author(s): Bergami G

Publication type: Article

Publication status: Published

Journal: Logics

Year: 2024

Volume: 2

Issue: 2

Pages: 79-111

Online publication date: 31/05/2024

Acceptance date: 29/05/2024

Date deposited: 31/05/2024

ISSN (electronic): 2813-0405

Publisher: MDPI

URL: https://doi.org/10.3390/logics2020004

DOI: 10.3390/logics2020004

Data Access Statement: The code resulting from Reducer is freely available at: https://github. com/gyankos/reducer/releases/tag/v1.0 (Available on 18 May 2024).


Altmetrics

Altmetrics provided by Altmetric


Share