Proving partial order properties

AbstractA temporal verification method which is based upon partial order semantics of traces (Mazurkiewicz, 1987) is presented. The semantic model used here can express the distributed aspects of a program, e.g. properties such as serializability of database transactions, layering of a program, snapshots or the parallel execution of program segments. The proof rules are shown to be sound and relatively complete