---
title: "DECLARE Manual"
type: source
tags: [bpm, declarative, declare, condec, decserflow, ltl, workflow, tool-manual]
authors: [Pesic, Maja; Schonenberg, Helen; van der Aalst, Wil M. P.]
year: 2008
venue: "Eindhoven University of Technology — prototype tool manual (is.tm.tue.nl/staff/mpesic)"
kind: manual
raw_path: "raw/Process Frameworks & BPM/DECLARE manual.pdf"
sources: []
key_claims:
  - "DECLARE is a prototype Workflow Management System implementing a declarative (constraint-based) approach to business process modelling, specification and enactment of loosely-structured processes."
  - "Core contrast with imperative languages: traditional notations specify HOW (directed control-flow graphs with fixed begin/end); DECLARE specifies WHAT via constraints — any execution that does not violate the constraints is allowed."
  - "Formal foundation is Linear Temporal Logic (LTL); constraints are translated into finite-state automata (via standard LTL-to-automata model-checking algorithms) which DECLARE uses for verification and enactment."
  - "Constraint templates are grouped into named sets (languages) — shipped sets are ConDec and DecSerFlow — and users can define new templates with custom LTL formulas."
  - "Architecture: DECLARE can run stand-alone or integrated with YAWL (imperative, highly-structured operational processes) and ProM (process mining); DECLARE logs feed ProM, ProM can export discovered DECLARE models back for conformance checking."
  - "Runtime constraint states are visualised three-valued: green (satisfied), orange (temporarily violated but repairable), red (permanently violated); constraint types = mandatory, optional, conditional."
  - "Model-level verification: dead-activity detection, conflicting-constraints detection, history validation (checking a past trace against the model)."
  - "Recommendation service (novel): at run-time DECLARE can recommend next activities to the user based on past execution history, to navigate the space of permitted options."
  - "Distribution: Java-based; two modules — declareService (web service for YAWL interface B, Tomcat-hosted) and declare itself (designer.bat, framework.bat, worklist.bat); GNU-licensed; dated 18 Feb 2008."
  - "DECLARE supports organisational perspective (users, roles, authorisations) and data perspective (typed data elements, mapped to/from YAWL data at case start/close) in addition to control-flow constraints."
created: 2026-04-15
updated: 2026-04-15
---

# 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
```

## 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]].