System modelling with high-level Petri nets

A linear-algebraic techniques for verifying invariant assertions are used, yielding a calculus of S-invariants for PrT-nets, and these modelling and analysis techniques are applied to a scheme for organizing a distributed data base taken from literature.

Abstract

The paper presents a high-level Petri net model of concurrent systems called predicate /transition-nets (PrT-nets). Its places represent variable properties of, or relations between, individuals; they are 'predicates' with variable extension. The transitions represent classes of elementary changes of those extensions. The model is introduced on the basis of a simple example from resource management. The central part of the paper is devoted to linear-algebraic techniques for verifying invariant assertions, yielding a calculus of S-invariants for PrT-nets. Finally, these modelling and analysis techniques are applied to a scheme for organizing a distributed data base taken from literature.