Foundations of Reactive Synthesis for Declarative Process Specifications
Authors: Luca Geatti, Marco Montali, Andrey Rivkin
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | In this paper we study, for the first time, the foundations of reactive synthesis for DECLARE, a well-established declarative, pattern-based business process modelling language grounded in LTLf. We provide a threefold contribution. First, we define a reactive synthesis problem for DECLARE. Second, we show how an arbitrary DECLARE specification can be polynomially encoded into an equivalent pure-past one in LTLf, and exploit this to define an EXPTIME algorithm for DECLARE synthesis. Third, we derive a symbolic version of this algorithm, by introducing a novel translation of pure-past temporal formulas into symbolic deterministic finite automata. and Second, we intend to perform a large-scale experimental evaluation of our symbolic procedure, using different symbolic reachability game solvers and contrasting it with explicit approaches. |
| Researcher Affiliation | Academia | University of Udine Free University of Bozen-Bolzano Technical University of Denmark |
| Pseudocode | Yes | Algorithm 1 synth-DECLARE |
| Open Source Code | No | The paper does not provide an unambiguous statement or link for the open-source code for the methodology described. It refers to existing tools but not to their own implementation. |
| Open Datasets | No | The paper describes theoretical algorithms and complexity results and does not involve empirical evaluation on a dataset. |
| Dataset Splits | No | The paper is theoretical and does not involve empirical evaluation or dataset splits. |
| Hardware Specification | No | The paper is theoretical and does not report on experiments, thus no hardware specifications are provided. |
| Software Dependencies | No | The paper mentions several tools (e.g., BLACK, Safety Synth, Demiurge) that were used or are relevant for the domain, but it does not provide specific version numbers for these or any other software dependencies required to reproduce their theoretical work or algorithms. |
| Experiment Setup | No | The paper presents theoretical algorithms and complexity analysis, and explicitly mentions future work for experimental evaluation, thus no experimental setup details are provided. |