Decompositional Minimisation of Monolithic Processes

Research output: Contribution to journalArticleAcademic

22 Downloads (Pure)

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.
Original languageEnglish
Article number2012.06468
Number of pages24
JournalarXiv
Volume2020
DOIs
Publication statusPublished - 11 Dec 2020

Bibliographical note

24 pages, technical report

Keywords

  • cs.LO

Fingerprint

Dive into the research topics of 'Decompositional Minimisation of Monolithic Processes'. Together they form a unique fingerprint.

Cite this