A verification algorithm for Declarative Concurrent Programming

TL;DR

This paper introduces Declarative Concurrent Programming (DCP), a novel verification algorithm for distributed systems that uses causal compression to efficiently verify large concurrent processes, outperforming traditional methods.

Contribution

The paper presents a new verification approach based on causal compression and event structures, significantly improving efficiency for verifying distributed concurrent systems.

Findings

Causal compression reduces verification complexity.

Benchmarks show DCP handles more agents than traditional methods.

DCP is efficient in both time and space for classic concurrency problems.

Abstract

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.