Research map / Learning theory and algorithms / Combinatorial and search optimization
Foundations of Reactive Synthesis for Declarative Process Specifications
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Formalizes reactive synthesis for DECLARE process specifications over simple LTLf traces, gives a polynomial pastification of DECLARE patterns yielding an EXPTIME algorithm, and a symbolic DFA-based version.
Problem
Reactive synthesis for declarative DECLARE business process specifications (grounded in LTLf) has not been studied; generic LTLf synthesis is 2EXPTIME-complete, so a more efficient, assume-guarantee formulation is needed.
Approach
Defines assume-guarantee realizability/synthesis for DECLARE over simple finite traces, shows every DECLARE pattern admits a linear-size pure-past rewriting ("pastification"), and builds linear-size symbolic DFAs from pure-past formulas so synthesis reduces to a symbolic reachability game in singly exponential time.
Key results
- Every DECLARE pattern admits a pastification of size linear in the input, implying DECLARE realizability is in EXPTIME (Theorem 4, Theorem 6).
- Symbolic DFA construction from pure-past LTLf formulas yields linear-size symbolic DFAs (Theorem 7).
- Contrasts with 2EXPTIME-completeness of full LTLf realizability, since LTLf pastification is not polynomial in general.
Surprising findings
- Full LTLf does not admit polynomial-size pastification, unlike DECLARE.
Limitations
- No experimental evaluation of the symbolic procedure; efficiency is only theoretical.
- Results are stated for single-action patterns; boolean combinations of actions are only claimed to be covered.
Experimental setup
Baselines: naive 2EXPTIME LTLf synthesis reduction
Builds on: LTLf synthesis DECLARE symbolic automata encoding of LTLf reachability games
Closest papers by meaning
- Adaptive Reactive Synthesis for LTL and LTLf Modulo Theories (AAAI 2024 · similarity 0.89)
- Linear-Time Verification of Data-Aware Processes Modulo Theories via Covers and Automata (AAAI 2024 · similarity 0.86)
- LTLf Synthesis Under Unreliable Input (AAAI 2025 · similarity 0.85)
- First-Order Automata (AAAI 2025 · similarity 0.84)
- LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments (AAAI 2025 · similarity 0.83)
- Situation Calculus Temporally Lifted Abstractions for Generalized Planning (AAAI 2025 · similarity 0.83)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.