Satisfiability of Dataflow Models of Distributed Programs

The satisfiability problem is discussed for dataflow models of distributed programs represented as processes communicating with each other by exchanging messages through buffers such that each process is initiated as soon as the data are ready for use. The satisfiability means that, when exchanging messages of different kind, parameters of the buffers are coordinated such that any admissible process histories do not result in appearance of deadlock situations, when the communicating processes block each other. The satisfiability problem reduces to finding a stable and irredundant marking of marked nets of special form. Such a marking prevents program hangups for any admissible program histories.