Imperative process algebra with abstraction

This paper introduces an imperative process algebra. It concerns an extension of ACP (Algebra of Communicating Processes) with features to change data in the course of a process, to proceed at certain stages of a process in a way that depends on data, and to communicate data between processes. This process algebra 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 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.