The analysis of distributed systems by means of predicate/transition-nets

Abstract

Within the framework of net-semantics of models of dynamic systems, the present paper introduces a new standard interpretation of nets called predicate/transition-nets (Pr/T-nets). These nets are schemes of ‘ordinary’ Petri nets. The places (circles) of Pr/T-nets represent changing properties of, or relations between, individuals; they are ‘predicates’ with variable extension. A current case of a system modelled by a Pr/T-net is denoted by marking the places with those tuples of individual symbols for which the respective predicates hold in that case. The transitions (boxes) are schemes of elementary changes of markings constituting the processes carried by the system. Instances of these schemes are generated by means of consistent substitution of individual variables by symbols.

Assuming some familiarity with Petri nets, the paper first introduces the predicate/transition-net model in its most general form, from which some special cases are derived. Then it is shown that the ‘dead’ transitions of a Pr/T-net represent first-order formulas expressing invariant assertions about the modelled systems. Next the linear-algebraic techniques for finding invariants are transferred to Pr/T-nets. The last part of the paper is devoted to the analysis of a scheme for organizing distributed database systems.