A Geometric Approach to the Problem of Unique Decomposition of Processes

TL;DR

This paper introduces a geometric method for uniquely decomposing concurrent processes, providing a factorization theorem and an algorithm implemented in the ALCOOL static analyzer.

Contribution

It presents a novel geometric approach to prime decomposition of concurrent processes, including a proof of unique factorization and an effective algorithm.

Findings

Proves a unique factorization theorem for concurrent processes using cubical areas.

Develops an algorithm for process decomposition that is correct and complete.

Implements the algorithm in the ALCOOL static analyzer.

Abstract

This paper proposes a geometric solution to the problem of prime decomposability of concurrent processes first explored by R. Milner and F. Moller in [MM93]. Concurrent programs are given a geometric semantics using cubical areas, for which a unique factorization theorem is proved. An effective factorization method which is correct and complete with respect to the geometric semantics is derived from the factorization theorem. This algorithm is implemented in the static analyzer ALCOOL.