Priorities in process algebras
type: Item
instance of: scholarly article
title: Priorities in process algebras
zbMATH Open document ID: 0726.68053
DOI: 10.1016/0890-5401(90)90059-Q
author: Rance Cleaveland
author: Matthew Hennessy
published in: Information and Computation
publication date: 1990-01-01T00:00:00Z
review text: 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^{\a…
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68Q10
Mathematics Subject Classification ID: 68Q85
zbMATH DE Number: 4199643
zbMATH Keywords: calculus of communicating systems
zbMATH Keywords: process algebras
zbMATH Keywords: concurrent systems
zbMATH Keywords: observational equivalence
zbMATH Keywords: operational semantics
zbMATH Keywords: labeled transition system
zbMATH Keywords: behavioral equivalence
describes a project that uses: Ada95
MaRDI profile type: Publication
cites work: Q4727412
cites work: Process algebra for synchronous communication
cites work: Testing equivalences for processes
cites work: Statecharts: a visual formalism for complex systems
cites work: Algebraic laws for nondeterminism and concurrency
cites work: Q3777424
cites work: CCS expressions, finite state processes, and three problems of equivalence
cites work: A calculus of communicating systems
cites work: Calculi for synchrony and asynchrony
cites work: Three Partition Refinement Algorithms
cites work: Q3694687
description: scientific article; zbMATH DE number 4199643