A new class of high-level Petri nets is defined, which is a combination of predicate transition nets and first order temporal logic. By combining these two formal methods, one can explicitly specify the structures and specify and verify various properties of parallel and distributed systems in the same framework, which cannot be achieved by using either one of the formal methods individually. Therefore, a more powerful methodology for the specification and the verification of parallel and distributed systems is obtained. The application of temporal predicate transition nets is illustrated through the specification and the verification of the five-dining-philosophers problem.
