DECLARE

DECLARE is both (a) a family of declarative, constraint-based process-modelling languages (ConDec, DecSerFlow, and user-defined template sets) and (b) the prototype WfMS that enacts them, developed by Maja Pesic, Helen Schonenberg and Wil van der Aalst at TU Eindhoven (sources/2008-pesic-declare-manual). It is the canonical counterpart to imperative notations like frameworks/bpmn for loosely-structured, knowledge-intensive processes.

Paradigm

A DECLARE model is a set of LTL constraints over a vocabulary of activities. Execution semantics is "everything not forbidden is allowed": any trace that satisfies all constraints is legal. Control-flow is therefore implicit rather than encoded as a directed graph (sources/2008-pesic-declare-manual, §1.1).

WHAT not HOW — the model specifies what must/must-not hold; the order of work is an emergent property of the constraint set.
Avoids over-specification for flexible processes where imperative models force frequent deviations from the prescribed flow.

Formal foundation

Constraints compile to LTL formulas (over finite traces in practice — LTLf).
LTL formulas are translated to finite-state automata via standard model-checking algorithms; DECLARE uses these automata for verification and run-time enactment (sources/2008-pesic-declare-manual, §1.1).

Constraint templates

Constraints are instantiated from reusable templates, each a parameterised LTL formula. Shipped template sets:

ConDec (business processes)

Conventional grouping:

Existence — existence(A), absence(A), exactly(n,A), init(A).
Relation / bi-relation — responded existence(A,B), co-existence(A,B), response(A,B) (if A then eventually B after), precedence(A,B), succession(A,B), and their chain variants (chain response, chain precedence, chain succession) requiring immediate adjacency.
Negation — not co-existence, not succession, not chain succession.

(Template naming follows the standard ConDec literature referenced by the manual; the manual pages read list the sets but do not enumerate every template.)

DecSerFlow (service choreographies)

Same template mechanism applied to inter-organisational service flows.

User-defined templates

New templates can be added by supplying an LTL formula; constraints may also carry data conditions (appendix B of the manual).

Constraint typing & run-time state

Type: mandatory · optional · conditional.
Run-time state (traffic light): green = satisfied; orange = currently violated but still repairable by future activity; red = permanently violated (sources/2008-pesic-declare-manual, §5.1.2).

Tool — DECLARE prototype

Java, GNU-licensed (is.tm.tue.nl/staff/mpesic), three desktop apps:

Designer (designer.bat) — author activities, constraints, roles/users, and data; select a constraint-template set per model.
Framework (framework.bat) — case management, assignment models, run-time model change (migrate all instances).
Worklist (worklist.bat) — participant client for executing cases.
declareService.war — YAWL integration web-service (interface B, Tomcat).

Perspectives supported

Work — activities + constraints.
People — users, roles, authorisations.
Data — typed data elements; I/O mapping to/from YAWL data at case start/close.

Model-level verification

Dead activity detection — an activity the constraints render unreachable.
Conflicting constraints — no trace satisfies all constraints.
History validation — check a past trace against the model.

Run-time services

Warnings about possible future violations.
Recommendation service — at each step, recommend next activities based on past executions (history-driven navigation of the permitted-behaviour space).

Ecosystem integration

DECLARE (loosely-structured) ── event logs ──→ ProM ── language/model export ──→ DECLARE
           ▲                                     │
           └────── YAWL (highly-structured) ─────┘
DECLARE (loosely-structured) ── event logs ──→ ProM ── language/model export ──→ DECLARE
           ▲                                     │
           └────── YAWL (highly-structured) ─────┘

YAWL — hosts highly-structured parent processes; DECLARE models act as loosely-structured sub-processes.
ProM — declarative process discovery (e.g. Declare Miner, later DisCoveR) and conformance checking against DECLARE models. See methods/process-mining-basics and concepts/process-discovery.

Role in the wider BPM landscape

Canonical declarative counterpart to imperative frameworks/bpmn — see concepts/declarative-process-modelling for the paradigm.
Shares flexibility goals with frameworks/cmmn (case management) but keeps a formal LTL grounding.
Orthogonal to frameworks/dmn, which targets decision logic rather than control-flow constraints.

Extensions (post-2008, referenced-not-ingested)

Declare Miner and variants (Maggi et al.) — automated discovery of DECLARE models from logs.
MP-Declare / Data-aware Declare — data-conditional constraints (Burattin, Maggi, Sperduti; Montali et al.).
LTLf / LDLf semantics — De Giacomo & Vardi formalisation adopted retroactively.

Authors / hub entities

entities/wil-van-der-aalst · Maja Pesic · Helen Schonenberg · downstream hubs entities/fabrizio-maggi, entities/marco-montali.