Priorities in process algebras (Q802881)

The paper tries to give a semantic theory of programming languages constructs which embody the notion of priority between actions, by a modified form of labeled transition systems. The syntax of the langage is essentially that of pure \(CCS^ 1\). Starting from the (countable) set of action labels \(\Lambda\), the set \({\mathcal A}=\Lambda \cup {\bar \Lambda}\cup \{\tau \}\) is constructed, taking an isomorphic copy \({\bar \Lambda}\) of \(\Lambda\). Then, a prioritized version a of each \(a\in {\mathcal A}\) is added, obtaining the final set of actions, \({\mathcal A}ct={\mathcal A}\cup \underline {\mathcal A}\), on which the set of terms is constructed, with the following syntax: \(t::=nil| a\cdot t| t| t\;| t+t| \;t\setminus \lambda \;t[R]\;| x| \;fix(x\cdot t)\) where \({\mathcal R}: {\mathcal A}ct\to {\mathcal A}ct\) is a relabeling which preserves \(\tau\),\({\underline \tau}\) and priorities. Here and in the following, let \(\underline a,\underline b\in \underline {\mathcal A}\), \(a,b\in {\mathcal A}\), \(\alpha,\beta\in {\mathcal A}ct\), \(\lambda\in {\mathcal A}ct-\{\tau,{\underline \tau}\}.\) Processes are closed terms on this language, denoted by \(p,q,r\). In a first step, the operational semantics of the language is given without priorities, by a labeled transition system (l.t.s.) \(<P,\to,Act>\) where P is the set of processes, and \(\to\) represents a family of relations \(\to^{\alpha}\) defined by structural induction on terms. Then, a new system \(<P,\to,Act>\) is defined, by eliminating transitions of the form \(p\to^{a}q\) which cannot occur, since the process p can evolve in a process \(q'\) by an action \(\underline b\) which has priority on a. As usual, an important concept is that of behavioral equivalence between processes. In absence of priorities, \(<P,\to,Act>\) admits a strong behavioral equivalence \(\approx\), defined as the largest bisimulation, i.e. the largest symmetric relation \(R\subseteq PXP\) such that: \(p R q\) and \(p\to^{\alpha}p'\) implies \(q\to^{\alpha}q'\) for some \(q'\) such that \(p' R q'.\) The analogous relation \(\approx_ p\) for the l.t.s. \(<P,\to,Act>\) with priorities is not adequate, because it identifies processes that can intuitively be distinguished. In order to avoid this difficulty, another operational semantics, based on a new relation \(\mapsto\), is introduced. In this definition, transitions of the form \(p\mapsto^{a}\) q are forbidden when there exist a \(q'\) such that \(p\to^{\tau}q'.\) The main theorem states that the strong equivalence \(\simeq\) generated by the l.t.s. \(<P,\mapsto,Act>\) is a congruence with respect to the operators of CCS, as well as to the operators corresponding to prioritization and deprioritization of actions,and hence it is an adequate notion of behavioral equivalence. Two examples, the well known Alternating bit protocol and a system consisting of a process X that flips back and forth between two states and a process C that checks that X is running properly, illustrate the approach, which appears to be a significant step towards a better understanding of priorities and their semantics.