AbstractThis paper formalizes the operation of a monitor—one of the fundamental models for concurrent processing—in a framework which is an extension of CCS (the calculus of communication systems) proposed by Milner. The purpose of this paper is to define the mutual exclusion and synchronization control of a monitor based on formal computation mechanisms and to provide a basis for the verification of the properties of a monitor as a concurrent program.For this purpose, a programming language which directly represents the execution mechanism of the monitor and the syntactical translation from that language to a CCS expression are defined. Through this translation, the mutual exclusion of the monitor procedure as well as synchronization control by means of the conditional variable—the essential features of the monitor—are formalized within the CCS framework. As a result, by adopting an observable equivalence relation between the semantics of CCS operational expressions of the semantics of operation of the model, we show that it is possible to demonstrate the abstraction mechanism of th