From Nets to Logic and Back in the Specification of Processes

Among formal models proposed to specify concurrent systems and processes, three main groups emerged. They can be referred to as net models, algebraic calculi and process logics. Each group supports specific abstraction methodology and possesses different descriptive and analytical power. These two abilities are, to some extent, contradictory and usually are exploited separately in theoretical studies. However, their combination is highly desirable in practical tools for the verification and synthesis of systems. This stimulates the comparative studies of different classes of models with cross-interpretation of their basic notions and primitives. Some efforts to combine their advantages in the framework of unified theories are now in progress. The models based on Petri nets seem to be the most close to the adequate description of “pure” concurrency. As a result, many net- -based models were proposed for the formal specification and validation of concurrent systems: control structures in parallel programs, circuitry design, net protocols, etc. However, these models, providing a good insight into structural properties of designed concurrent systems, do not contain sufficient support for the validation of behavioural properties and equivalencies. This forces to have recources to some “external” formalisms. For example, having a net description of a system, we use firing sequences, traces, net languages, etc. to define and analyze the net properties. It would be more convenient if both descriptive and analytical parts of a modelling theory were based on the same set of basic notions and constructors.