Dataflow Analysis of Distributed Programs Using Generalized Marked Nets

The satisfiability and algorithmic decidability problems are discussed for message passing models of distributed programs represented as processes communicating through buffers. The satisfiability means that parameters of the buffers are coordinated such that any admissible process histories do not result in appearance of deadlock situations. The decidability problem is reduced to finding the least stable marking on upper semi-lattice of labels of arcs and vertices of the generalized marked net of the distributed program with alternative selections, switches and forks of dataflows. The labels are allowed to be of arbitrary semantic nature. The generalized marked nets represent an algorithmically decidable class of dataflow models of distributed programs.