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 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.
Preprint available:
arXiv:2103.07863v5 [cs.LO]