Priority and abstraction in process algebra

TitlePriority and abstraction in process algebra
Publication TypeJournal Articles
Year of Publication2007
AuthorsCleaveland R, Lüttgen G, Natarajan V
JournalInformation and Computation
Pagination1426 - 1458
Date Published2007/09//
ISBN Number0890-5401
KeywordsAxiomatization, Bisimulation, Full abstraction, Observation congruence, Priority, Process algebra

More than 15 years ago, Cleaveland and Hennessy proposed an extension of the process algebra CCS in which some actions may take priority over others. The theory was equipped with a behavioral congruence based on strong bisimulation.This article gives a full account of the challenges in, and the solutions employed for, defining a semantic theory of observation congruence for this process algebra. A full-abstraction result is presented whose proof relies on a novel approach based on successive approximations for identifying the largest congruence contained in an intuitive but naïve equivalence. Prioritized observation congruence is also characterized equationally for the class of finite processes, while its utility for system verification is demonstrated by an illustrative example.