Imperative process algebra with abstraction

TL;DR

This paper presents an imperative process algebra based on ACP that supports action abstraction, enabling new applications like information-flow security analysis, with proven soundness and semi-completeness results.

Contribution

It introduces an imperative process algebra with abstraction capabilities, extending existing frameworks and supporting security analysis.

Findings

Supports abstraction from non-visible actions

Establishes soundness and semi-completeness of axiomatization

Enables potential applications in security analysis

Abstract

This paper introduces an imperative process algebra based on ACP (Algebra of Communicating Processes). Like other imperative process algebras, this process algebra deals with processes of the kind that arises from the execution of imperative programs. It distinguishes itself from already existing imperative process algebras among other things by supporting abstraction from actions that are considered not to be visible. The support of abstraction of this kind opens interesting application possibilities of the process algebra. This paper goes briefly into the possibility of information-flow security analysis of the kind that is concerned with the leakage of confidential data. For the presented axiomatization, soundness and semi-completeness results with respect to a notion of branching bisimulation equivalence are established.