Decidability of the Analysis Problem for Dataflow Models of Programs

摘要

In the paper, algorithmic decidability of the analysis problem for dataflow models of programs is studied. The solution of the problem is the least stable marking on upper semi-lattice of labels of arcs and vertices of the generalized dataflow graph of the program. The labels are allowed to be of arbitrary semantic nature. Whether the analysis problem is decidable depends on properties of the marking function that interprets the analysis scheme given by a system of functional equations.