A Graph-Theoretic Characterization of the $\text{PV}_{\text{chunk}}$ Class of Synchronizing Primitives

Abstract

Many of the process synchronization problems studied in the literature are of the form of a conjunction of finitely many conditions of the type “process $p_i$ blocks process $p_j$”. Such problems may be expressed as directed graphs whose nodes represent the processes and where there is an edge from node i to node j if and only if process $p_i$ blocks process $p_j$. We characterize the class of graphs which correspond to the system of synchronizing primitives of Vantilborgh and van Lamsweerde in terms of a normal form representation and present an efficient algorithm for determining whether an arbitrary graph is in this class.