Decompositional Minimisation of Monolithic Processes

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademic

21 Downloads (Pure)

Samenvatting

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.
Originele taal-2Engels
Artikelnummer2012.06468
Aantal pagina's24
TijdschriftarXiv
Volume2020
DOI's
StatusGepubliceerd - 11 dec. 2020

Bibliografische nota

24 pages, technical report

Vingerafdruk

Duik in de onderzoeksthema's van 'Decompositional Minimisation of Monolithic Processes'. Samen vormen ze een unieke vingerafdruk.

Citeer dit