Foundations of Reactive Synthesis for Declarative Process Specifications
Luca Geatti, Marco Montali, Andrey Rivkin
Abstract
Given a specification of Linear-time Temporal Logic interpreted over finite traces (LTLf), the reactive synthesis problem asks to find a finitely-representable, terminating controller that reacts to the uncontrollable actions of an environment in order to enforce a desired system specification. 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.
BibTeX
@article{Geatti_Montali_Rivkin_2024, title={Foundations of Reactive Synthesis for Declarative Process Specifications}, volume={38}, url={https://ojs.aaai.org/index.php/AAAI/article/view/29690}, DOI={10.1609/aaai.v38i16.29690}, abstractNote={Given a specification of Linear-time Temporal Logic interpreted over finite traces (LTLf), the reactive synthesis problem asks to find a finitely-representable, terminating controller that reacts to the uncontrollable actions of an environment in order to enforce a desired system specification. 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.}, number={16}, journal={Proceedings of the AAAI Conference on Artificial Intelligence}, author={Geatti, Luca and Montali, Marco and Rivkin, Andrey}, year={2024}, month={Mar.}, pages={17416-17425} }