Equivalence checking of Petri net models of programs using static and dynamic cut-points (Q2415374)

Semantics-preserving transformation -- and in particular parallelization -- is an interesting and non-trivial problem of programs since the 1970s. This paper suggests executing this kind of transformation on models of the involved programs. The authors chose the modeling technique of coloured Petri nets (CPN), rightly justifying their choice by CPN's capacity to cope with data, to explicitly model concurrent behavior, and to sharply formulate (wanted and unwanted) properties. In CPN, data are represented by variables as they are in logic, not by store-like variables as they occur in programs. The paper demonstrates that this allows data dependencies to be depicted more directly thus making CPN particularly convenient as intermediate representations (IRs) of both the source and the transformed codes. The paper starts with restricting the general CPN model to a version sufficient for the intended use cases. In particular, sets of parallelizable transitions are introduced. A core notion is computational equivalence between CPN models and the notion of (static and dynamic) cut points, used to cut computation sequences into pieces, and to construct equivalent computations piece-wise. Much effort is spent to describe efficient algorithms that for a given program construct an equivalent program with the wanted properties. All transformation algorithms are implemented, and experimental measurement results are presented in detail with the intention to show the algorithms' efficiency. Correctness arguments for the algorithms are moved to the appendix. Altogether, this is an interesting and convincing approach. It is a pity that the English style is occasionally poor, thus reducing readability.