Decompositional Minimisation of Monolithic Processes

TL;DR

This paper introduces a novel decompositional minimisation technique for monolithic processes with data, enabling effective property preservation and analysis by splitting a complex process into simpler, parameter-specific components.

Contribution

It presents a method to decompose monolithic processes with data into smaller processes, preserving properties and improving static analysis capabilities.

Findings

Decomposition preserves properties of the original monolithic process.

State invariants enhance the effectiveness of the decomposition.

Applied technique successfully to multiple specifications.

Abstract

Compositional minimisation can be an effective technique to reduce the state space explosion problem. This technique considers a parallel composition of several processes. In its simplest form, each sequential process is replaced by an abstraction, simpler than the corresponding process while still preserving the property that is checked. However, this technique cannot be applied in a setting where parallel composition is first translated to a non-deterministic sequential monolithic process. The advantage of this monolithic process is that it facilitates static analysis of global behaviour. Therefore, we present a technique that considers a monolithic process with data and decomposes it into two processes where each process defines behaviour for a subset of the parameters of the monolithic process. We prove that these processes preserve the properties of the monolithic process under a suitable synchronisation context. Moreover, we prove that state invariants can be used to improve its effectiveness. Finally, we apply the decomposition technique to several specifications.