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)

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

Conference

Conference38th AAAI Conference on Artificial Intelligence
Country/TerritoryCanada
CityVancouver
Period20/02/202427/02/2024
SeriesProceedings of the Aaai Conference on Artificial Intelligence
ISSN2374-3468

Fingerprint

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

Cite this