Foundations of Reactive Synthesis for Declarative Process Specifications

Luca Geatti, Marco Montali, Andrey Rivkin

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

1 Downloads (Pure)


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.
Original languageEnglish
Title of host publicationProceedings of the 38th AAAI Conference on Artificial Intelligence
PublisherAAAI Press
Publication date2024
ISBN (Electronic)978-1-57735-887-9
Publication statusPublished - 2024
Event38th AAAI Conference on Artificial Intelligence - Vancouver , Canada
Duration: 20 Feb 202427 Feb 2024


Conference38th AAAI Conference on Artificial Intelligence
SeriesProceedings of the Aaai Conference on Artificial Intelligence


Dive into the research topics of 'Foundations of Reactive Synthesis for Declarative Process Specifications'. Together they form a unique fingerprint.

Cite this