DECLARE Manual (2008)

Summary

User/installation manual for the DECLARE prototype, the reference implementation of the declarative-process-modelling paradigm developed at TU Eindhoven. DECLARE is a constraint-based WfMS: a process model is a set of LTL constraints over activities rather than a directed control-flow graph. Any trace that satisfies the constraints is a legal execution, so the control-flow is specified implicitly — well-suited to loosely-structured, knowledge-intensive, or flexibility-requiring processes where imperative models induce over-specification and frequent deviations (sources/2008-pesic-declare-manual, ch. 1).

The manual covers: installation (Java, Apache Tomcat, YAWL integration via declareService.war); the Designer (model authoring with activities + constraints drawn from a chosen template set — ConDec or DecSerFlow); the Framework (case manager) and Worklist (execution client); and integration with YAWL and ProM. Formal semantics: each constraint template is an LTL pattern; models are checked and enacted via LTL→finite-state-automata translation. At run-time, constraints carry a traffic-light state (green/orange/red) reflecting satisfied / temporarily-violated-but-repairable / permanently-violated, together with a typing of mandatory, optional, or conditional.

Distinctive capabilities surfaced in the manual:

Verification of a DECLARE model for dead activities, conflicting constraints, and history validation.
Run-time constraint monitoring with warnings about possible future violations.
Recommendation service — advises the user on the next activity based on past executions, turning the permitted-behaviour space into a navigable one.
Multi-perspective modelling — work (activities + constraints), people (users/roles/authorisations), data (typed data elements mapped from/to YAWL).
Run-time adaptation — the case model can be changed mid-case (migrate all instances / save model), with re-verification.

Appendices document LTL syntax and constraint-condition syntax (data conditions attached to constraints).

Architecture (Fig. 1.2)

operational process
  ├── highly-structured ──→ YAWL ──┐
  └── loosely-structured ─→ DECLARE ─┤── event logs ──→ ProM
                                     │                      │
                              recommendation ←── language/model export
operational process
  ├── highly-structured ──→ YAWL ──┐
  └── loosely-structured ─→ DECLARE ─┤── event logs ──→ ProM
                                     │                      │
                              recommendation ←── language/model export

Constraint template sets

ConDec — the canonical template set for business processes; includes existence (e.g. existence, absence, exactly, init), relation (response, precedence, succession, co-existence, responded existence), negation (not succession, not co-existence, not chain succession), and chain variants (chain response, chain precedence, chain succession). (Specific template names inferred from the standard ConDec literature; the manual references the set but does not exhaustively list templates in the pages read.)
DecSerFlow — declarative service-flow language; same template mechanism applied to service choreographies.
Users can define additional templates by supplying LTL formulas.

Key claims

See frontmatter.

Open questions / unread

Exhaustive constraint-template catalogue (ConDec full list with LTL formulas) — lives in the cited ConDec/DecSerFlow papers rather than this manual; manual appendix A gives LTL syntax, appendix B gives constraint-condition (data-predicate) syntax (not fully extracted in this ingest).
Which LTL variant — the manual leaves the reference unresolved ([?]); the ConDec literature uses LTL over finite traces (LTLf), later formalised by De Giacomo & Vardi.

Connections

Defines the tool behind frameworks/declare and concepts/declarative-process-modelling.
Authors link to entity pages entities/wil-van-der-aalst; the broader DECLARE research line extends to entities/fabrizio-maggi (declarative discovery / Declare Miner) and entities/marco-montali (data-aware declarative reasoning).
Integrates with YAWL (imperative) and ProM — see methods/process-mining-basics; DECLARE models can be discovered from logs (declarative process discovery — concepts/process-discovery).
Counterpart to imperative frameworks/bpmn; shares "what-not-how" spirit with frameworks/cmmn and rule-layer frameworks/dmn.