Read Operators and their Expressiveness in Process Algebras

TL;DR

This paper explores two methods to incorporate non-blocking reading actions into PAFAS, a process algebra, analyzing their semantics, expressiveness, and potential for translation between variants.

Contribution

It introduces two read operators with different semantics into PAFAS and compares their expressiveness, providing laws to facilitate translation and further study.

Findings

The read-set prefix has simpler semantics but is syntactically restricted.

Processes with the second read operator can be translated into the first with timed-bisimilar behavior.

Open problem remains whether the first algebra is more expressive than the second.

Abstract

We study two different ways to enhance PAFAS, a process algebra for modelling asynchronous timed concurrent systems, with non-blocking reading actions. We first add reading in the form of a read-action prefix operator. This operator is very flexible, but its somewhat complex semantics requires two types of transition relations. We also present a read-set prefix operator with a simpler semantics, but with syntactic restrictions. We discuss the expressiveness of read prefixes; in particular, we compare them to read-arcs in Petri nets and justify the simple semantics of the second variant by showing that its processes can be translated into processes of the first with timed-bisimilar behaviour. It is still an open problem whether the first algebra is more expressive than the second; we give a number of laws that are interesting in their own right, and can help to find a backward translation.