Process Algebra with Autonomous Actions
This paper introduces autonomous observable actions into process
algebra. These actions can be observed but cannot be controlled by
an environment. The proposed extension of ACP allows verifications
without silent steps and fairness assumptions. The inclusion of
inequalities makes it possible to verify that an implementation
satisfies a given specification, with the specification indicating
exactly where the implementation may reduce nondeterminism.
(postscript /
pdf version of the complete paper)
Back to the list of Technical Reports.