  A verification method for distributed systems based on decoupling forward and
backward behaviour is proposed. This method uses an event structure based
algorithm that, given a CCS process, constructs its causal compression relative
to a choice of observable actions. Verifying the original process equipped with
distributed backtracking on non-observable actions, is equivalent to verifying
its relative compression which in general is much smaller. We call this method
Declarative Concurrent Programming (DCP). DCP technique compares well with
direct bisimulation based methods. Benchmarks for the classic dining
philosophers problem show that causal compression is rather efficient both
time- and space-wise. State of the art verification tools can successfully
handle more than 15 agents, whereas they can handle no more than 5 following
the traditional direct method; an altogether spectacular improvement, since in
this example the specification size is exponential in the number of agents.
