The authors wish to verify workflows designed using timed workflow nets, which Ling and Schmidt proposed in 2000 [1]. Boucheneb, the first author listed, and Rakkay proposed an abstraction technique of contracted state class graphs in 2008 [2]. In this paper, for the first time, Boucheneb and Barkaoui combine this with partial order reduction, proposed by Peled and Wilke in 1997 [3] and applied to timed systems by Belluomini and Myers in 2000 [4], to obtain a reduced state class graph. Soundness of the new technique is verified.

This is technical work in a difficult area. In a complicated model such as the one the authors are considering, the question of applicability is important. To answer this, the authors consider some examples and give experimental results that show how their technique performs compared to their own earlier work and earlier work by others.