---
title: DECLARE (Declarative Workflow Language & Tool)
type: framework
tags: [bpm, declarative, constraint-based, ltl, condec, decserflow, modelling]
sources: ["[[sources/2008-pesic-declare-manual]]"]
created: 2026-04-15
updated: 2026-04-15
---

# 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) ─────┘
```
- **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]].